diff options
| author | Matthieu Sozeau | 2014-09-24 22:25:49 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-24 22:25:49 +0200 |
| commit | 5a9aa1b1957ca27a7684dbc307ff7bf57317929f (patch) | |
| tree | d47454ab2508f6dcb04bf81e6b5c7e8f29a3cdd2 /tactics | |
| parent | 31e4222d35b614efa94a1d68b5d6491ea9e46bfa (diff) | |
Rename eq_constr functions in Evd to not break backward compatibility
with existing ML code.
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 |