From 42bed627c4a1c5a1ecf59d4865fc872b5eee7290 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 7 Sep 2018 12:22:17 +0200
Subject: Retroknowledge: simpler parsing rules

---
 plugins/ltac/extraargs.mli | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'plugins/ltac/extraargs.mli')

diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index e477b12cd3..fa70235975 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -72,11 +72,6 @@ val test_lpar_id_colon : unit Pcoq.Entry.t
 
 val wit_test_lpar_id_colon : (unit, unit, unit) Genarg.genarg_type
 
-(** Spiwack: Primitive for retroknowledge registration *)
-
-val retroknowledge_field : Retroknowledge.field Pcoq.Entry.t
-val wit_retroknowledge_field : (Retroknowledge.field, unit, unit) Genarg.genarg_type
-
 val wit_in_clause :
   (lident Locus.clause_expr,
    lident Locus.clause_expr,
-- 
cgit v1.2.3