From 2ec78477c720ba3a5343b49f25cfa9c1639adbba Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 7 Sep 2018 17:34:11 +0200
Subject: Retroknowledge: use GlobRef.t instead of Constr.t as entry

---
 plugins/ltac/extratactics.ml4 | 15 ---------------
 1 file changed, 15 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 9538abcb18..8dad6260ae 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -544,21 +544,6 @@ END
 
 
 
-(**********************************************************************)
-(*spiwack : Vernac commands for retroknowledge                        *)
-
-VERNAC COMMAND EXTEND RetroknowledgeRegister CLASSIFIED AS SIDEFF
- | [ "Register" constr(c) "as" "int31" pre_ident(n) ] ->
-           [ let env = Global.env () in
-             let evd = Evd.from_env env in
-             let tc,_ctx = Constrintern.interp_constr env evd c in
-             let tc = EConstr.to_constr evd tc in
-             let f = Retroknowledge.(KInt31 (int31_field_of_string n)) in
-             Global.register f tc ]
-END
-
-
-
 (**********************************************************************)
 (* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as
   defined by Conor McBride *)
-- 
cgit v1.2.3