diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/extratactics.ml4 | 6 |
1 files changed, 2 insertions, 4 deletions
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 |