diff options
| author | herbelin | 2001-07-06 08:47:30 +0000 |
|---|---|---|
| committer | herbelin | 2001-07-06 08:47:30 +0000 |
| commit | 790243ed041f0626cd2d1613473b8f393ecccd56 (patch) | |
| tree | 56e72740630e17fbb5305982210dfc3ed73ce909 | |
| parent | 7b1375fa933adfcc7ccee591d1e581fe858e9716 (diff) | |
la conversion ne doit être testé dans evar_conv qu'en absence de evar
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1832 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/evarconv.ml | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 6783e70a4f..f40ad4dc00 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -56,15 +56,16 @@ let rec evar_conv_x env isevars pbty term1 term2 = let term1 = whd_castappevar sigma term1 in let term2 = whd_castappevar sigma term2 in (* - if eq_constr term1 term2 then + if eq_constr term1 term2 then true - else if (not(has_undefined_isevars isevars term1)) & - not(has_undefined_isevars isevars term2) - then - is_fconv pbty env (evars_of isevars) term1 term2 - else + else *) - (is_fconv pbty env sigma term1 term2) or + (* Maybe convertible but since reducing can erase evars which [evar_apprec]*) + (* could have found, we do it only if the terms are free of evar *) + (not (has_undefined_isevars isevars term1) & + not (has_undefined_isevars isevars term2) & + is_fconv pbty env (evars_of isevars) term1 term2) + or if ise_undefined isevars term1 then solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term1,term2) else if ise_undefined isevars term2 then |