From ab2560233f2e6fc8c26853af6991533d8d335e16 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 7 Sep 2018 11:34:32 +0200
Subject: Retroknowledge: remove the (unused) by clause

---
 plugins/ltac/extratactics.ml4 | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'plugins')

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
 
 
-- 
cgit v1.2.3