diff options
author | 2015-04-22 18:51:48 +0200 | |
---|---|---|
committer | 2015-04-22 18:55:13 +0200 | |
commit | 501d6dd5691474c807a722d9b5b6e3fa9d83c749 (patch) | |
tree | 959a4c35926f7b0e098cd82109b0bfde3f29ce3b /tactics | |
parent | 74d7dd7ae08dedfd80c056a345c1b3398eb91b5e (diff) |
Tactical `progress` compares term up to potentially equalisable universes.
Followup of: f7b29094fe7cc13ea475447bd30d9a8b942f0fef . In particular, re-closes #3593.
As a side effect, fixes an undiscovered bug of the `eq_constr` tactic which didn't consider terms up to evar instantiation.
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/extratactics.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 891e2dba5..7f0a4c660 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -772,7 +772,7 @@ END let eq_constr x y = Proofview.Goal.enter (fun gl -> let evd = Proofview.Goal.sigma gl in - if Evd.eq_constr_univs_test evd x y then Proofview.tclUNIT () + if Evarutil.eq_constr_univs_test evd evd x y then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "Not equal")) TACTIC EXTEND constr_eq |