diff options
| author | barras | 2008-11-21 12:57:44 +0000 |
|---|---|---|
| committer | barras | 2008-11-21 12:57:44 +0000 |
| commit | 9963243587e1e2af7737c85012200be84d645dad (patch) | |
| tree | 65b8563063883f48282731143dfb3815966973b3 | |
| parent | 32ad3a5570265c8f6fd437cb6e5d4bc56da0c06a (diff) | |
fixed exponential behavior of evar unif (ground case)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11612 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/evarconv.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index c682829087..efbe2f3358 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -164,10 +164,9 @@ let rec evar_conv_x env evd pbty term1 term2 = (* 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. Note: incomplete heuristic... *) - if is_ground_term evd term1 && is_ground_term evd term2 & - is_fconv pbty env (evars_of evd) term1 term2 + if is_ground_term evd term1 && is_ground_term evd term2 then - (evd,true) + (evd,is_fconv pbty env (evars_of evd) term1 term2) else let term1 = apprec_nohdbeta env evd term1 in let term2 = apprec_nohdbeta env evd term2 in |