Retroknowledge: remove the (unused) by clause

6 files changed, 27 insertions, 29 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 15f972afcf..95eea2d6b0 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -892,8 +892,8 @@ let retroknowledge f senv =
   Environ.retroknowledge f (env_of_senv senv)
 [@@@ocaml.warning "+3"]
 
-let register field value by_clause senv =
-  (* todo : value closed, by_clause safe, by_clause of the proper type*)
+let register field value senv =
+  (* todo : value closed *)
   (* spiwack : updates the safe_env with the information that the register
      action has to be performed (again) when the environment is imported *)
   { senv with
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 502e2970a1..2f83e71726 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -215,7 +215,7 @@ val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a
 [@@ocaml.deprecated "Use the projection of Environ.env"]
 
 val register :
-  field -> Retroknowledge.entry -> Constr.constr -> safe_transformer0
+  field -> Retroknowledge.entry -> safe_transformer0
 
 val register_inline : Constant.t -> safe_transformer0
 
diff --git a/library/global.ml b/library/global.ml
index e833f71142..5872126a12 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -271,8 +271,8 @@ let with_global f =
     push_context_set false ctx; a
 
 (* spiwack: register/unregister functions for retroknowledge *)
-let register field value by_clause =
-  globalize0 (Safe_typing.register field value by_clause)
+let register field value =
+  globalize0 (Safe_typing.register field value)
 
 let register_inline c = globalize0 (Safe_typing.register_inline c)
 
diff --git a/library/global.mli b/library/global.mli
index 2819c187ed..1708976222 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -148,7 +148,7 @@ val universes_of_global : GlobRef.t -> Univ.AUContext.t
 (** {6 Retroknowledge } *)
 
 val register :
-  Retroknowledge.field -> Constr.constr -> Constr.constr -> unit
+  Retroknowledge.field -> Constr.constr -> unit
 
 val register_inline : Constant.t -> unit
 
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index dc027c4041..2e932dd059 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -548,14 +548,12 @@ END
 (*spiwack : Vernac commands for retroknowledge                        *)
 
 VERNAC COMMAND EXTEND RetroknowledgeRegister CLASSIFIED AS SIDEFF
- | [ "Register" constr(c) "as" retroknowledge_field(f) "by" constr(b)] ->
+ | [ "Register" constr(c) "as" retroknowledge_field(f) ] ->
            [ let env = Global.env () in
              let evd = Evd.from_env env in
              let tc,_ctx = Constrintern.interp_constr env evd c in
-             let tb,_ctx(*FIXME*) = Constrintern.interp_constr env evd b in
              let tc = EConstr.to_constr evd tc in
-             let tb = EConstr.to_constr evd tb in
-             Global.register f tc tb ]
+             Global.register f tc ]
 END
 
 
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index 5c1c5d794d..f1b02759c5 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -45,8 +45,8 @@ Inductive int31 : Type := I31 : digits31 int31.
 (* spiwack: Registration of the type of integers, so that the matchs in
    the functions below perform dynamic decompilation (otherwise some segfault
    occur when they are applied to one non-closed term and one closed term). *)
-Register digits as int31 bits by True.
-Register int31 as int31 type by True.
+Register digits as int31 bits.
+Register int31 as int31 type.
 
 Declare Scope int31_scope.
 Declare ML Module "int31_syntax_plugin".
@@ -345,21 +345,21 @@ Definition lor31 n m := phi_inv (Z.lor (phi n) (phi m)).
 Definition land31 n m := phi_inv (Z.land (phi n) (phi m)).
 Definition lxor31 n m := phi_inv (Z.lxor (phi n) (phi m)).
 
-Register add31 as int31 plus by True.
-Register add31c as int31 plusc by True.
-Register add31carryc as int31 pluscarryc by True.
-Register sub31 as int31 minus by True.
-Register sub31c as int31 minusc by True.
-Register sub31carryc as int31 minuscarryc by True.
-Register mul31 as int31 times by True.
-Register mul31c as int31 timesc by True.
-Register div3121 as int31 div21 by True.
-Register div31 as int31 diveucl by True.
-Register compare31 as int31 compare by True.
-Register addmuldiv31 as int31 addmuldiv by True.
-Register lor31 as int31 lor by True.
-Register land31 as int31 land by True.
-Register lxor31 as int31 lxor by True.
+Register add31 as int31 plus.
+Register add31c as int31 plusc.
+Register add31carryc as int31 pluscarryc.
+Register sub31 as int31 minus.
+Register sub31c as int31 minusc.
+Register sub31carryc as int31 minuscarryc.
+Register mul31 as int31 times.
+Register mul31c as int31 timesc.
+Register div3121 as int31 div21.
+Register div31 as int31 diveucl.
+Register compare31 as int31 compare.
+Register addmuldiv31 as int31 addmuldiv.
+Register lor31 as int31 lor.
+Register land31 as int31 land.
+Register lxor31 as int31 lxor.
 
 Definition lnot31 n := lxor31 Tn n.
 Definition ldiff31 n m := land31 n (lnot31 m).
@@ -485,5 +485,5 @@ Definition tail031 (i:int31) :=
     end)
    i On.
 
-Register head031 as int31 head0 by True.
-Register tail031 as int31 tail0 by True.
+Register head031 as int31 head0.
+Register tail031 as int31 tail0.