diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/extratactics.ml4 | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 5 |
2 files changed, 4 insertions, 3 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 51ca5dddaa..0647fa8130 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -780,7 +780,7 @@ END let eq_constr x y = Proofview.Goal.enter (fun gl -> let evd = Proofview.Goal.sigma gl in - if Evd.eq_constr_test evd x y then Proofview.tclUNIT () + if Evd.eq_constr_univs_test evd x y then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "Not equal")) TACTIC EXTEND constr_eq diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 841116a0b4..f148104821 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4033,8 +4033,9 @@ let intros_transitivity n = Tacticals.New.tclTHEN intros (transitivity_gen n) (** d1 is the section variable in the global context, d2 in the goal context *) let interpretable_as_section_decl evd d1 d2 = match d2,d1 with | (_,Some _,_), (_,None,_) -> false - | (_,Some b1,t1), (_,Some b2,t2) -> e_eq_constr evd b1 b2 && e_eq_constr evd t1 t2 - | (_,None,t1), (_,_,t2) -> e_eq_constr evd t1 t2 + | (_,Some b1,t1), (_,Some b2,t2) -> + e_eq_constr_univs evd b1 b2 && e_eq_constr_univs evd t1 t2 + | (_,None,t1), (_,_,t2) -> e_eq_constr_univs evd t1 t2 let abstract_subproof id gk tac = let open Tacticals.New in |