diff options
| author | Vincent Laporte | 2018-09-07 11:34:32 +0200 |
|---|---|---|
| committer | Vincent Laporte | 2018-09-14 07:51:17 +0000 |
| commit | ab2560233f2e6fc8c26853af6991533d8d335e16 (patch) | |
| tree | a5712bb6310eb819f620a504b62533adf240cd94 /plugins | |
| parent | 4be2dd481c783bed7c09086b647d860e42b7ea9f (diff) | |
Retroknowledge: remove the (unused) by clause
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 |