diff options
| author | herbelin | 2011-03-31 18:58:15 +0000 |
|---|---|---|
| committer | herbelin | 2011-03-31 18:58:15 +0000 |
| commit | 3aad12391a9566af41395c674614e56383dff8c2 (patch) | |
| tree | eaf8d45f840bda673030e93946cf41487e357c2b | |
| parent | 6d10a4751154cfb8149398d37c8dbde775adbf1c (diff) | |
As remarked by Enrico, we'd better use eq_constr than structural equality
(it is a priori optimized but also able to reason modulo equality of
names and modulo alpha-conversion).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13945 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/evarconv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 6e92d74abb..b3b9ec3939 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -310,7 +310,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = | _, _ -> let f1 i = - if flex1 = flex2 then + if eq_constr flex1 flex2 then ise_list2 i (fun i -> evar_conv_x ts env i CONV) l1 l2 else (i,false) |