From 89a85a6603b7112e685a052d728284d3e4c2881e Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 11 May 2018 23:07:14 +0200 Subject: Fix #7421: constr_eq ignores universe constraints. The test isn't quite the one in #7421 because that use of algebraic universes is wrong. --- plugins/ltac/extratactics.ml4 | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index f2899ab63..660e29ca8 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -793,17 +793,12 @@ END (* ********************************************************************* *) -let eq_constr x y = - Proofview.Goal.enter begin fun gl -> - let env = Tacmach.New.pf_env gl in - let evd = Tacmach.New.project gl in - match EConstr.eq_constr_universes env evd x y with - | Some _ -> Proofview.tclUNIT () - | None -> Tacticals.New.tclFAIL 0 (str "Not equal") - end - TACTIC EXTEND constr_eq -| [ "constr_eq" constr(x) constr(y) ] -> [ eq_constr x y ] +| [ "constr_eq" constr(x) constr(y) ] -> [ Tactics.constr_eq ~strict:false x y ] +END + +TACTIC EXTEND constr_eq_strict +| [ "constr_eq_strict" constr(x) constr(y) ] -> [ Tactics.constr_eq ~strict:true x y ] END TACTIC EXTEND constr_eq_nounivs -- cgit v1.2.3