diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-17 22:26:18 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-17 22:26:18 +0200 |
| commit | d9736dae4168927f735ca4f60b61a83929ae4435 (patch) | |
| tree | 4afd85aee98945c458f210261ccc4265298e4475 /tactics/extratactics.ml4 | |
| parent | f96dc97f48df5d0fdf252be5f28478a58be77961 (diff) | |
Be more conservative and keep the use of eq_constr in pretyping/ functions.
Diffstat (limited to 'tactics/extratactics.ml4')
| -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 c1e6f42f1..51ca5ddda 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 evd x y then Proofview.tclUNIT () + if Evd.eq_constr_test evd x y then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "Not equal")) TACTIC EXTEND constr_eq |