diff options
| author | Vincent Laporte | 2018-09-07 17:34:11 +0200 |
|---|---|---|
| committer | Vincent Laporte | 2018-09-14 07:51:17 +0000 |
| commit | 2ec78477c720ba3a5343b49f25cfa9c1639adbba (patch) | |
| tree | ed8129ee7206bcb32c5e7d41830caf22b7cc2254 /plugins | |
| parent | 42bed627c4a1c5a1ecf59d4865fc872b5eee7290 (diff) | |
Retroknowledge: use GlobRef.t instead of Constr.t as entry
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/extratactics.ml4 | 15 |
1 files changed, 0 insertions, 15 deletions
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 @@ -545,21 +545,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 *) TACTIC EXTEND generalize_eqs |