diff options
| author | herbelin | 2007-10-01 07:41:34 +0000 |
|---|---|---|
| committer | herbelin | 2007-10-01 07:41:34 +0000 |
| commit | 251331283c7638a526c24643f5e3b42cdc5979e7 (patch) | |
| tree | b9f33cc77b19473275487930c17949b4a72c5b3e | |
| parent | c33c40d62a9b922863706d98e0e40b065107aaff (diff) | |
Amendement à la révision 10124 : déplacement de apprec_nohdbeta entre
is_fconv et le test d'équations simples (on admettra que is_fconv est
a priori plus efficace pour réduire que nohdbeta -- et de fait, sur
Stalmarck/algoRun, apprec_nohdbeta part en vrille alors que if_fconv
réussit vite).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10159 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/evarconv.ml | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index c4e3e6bdfc..9d0ae75e70 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -170,15 +170,19 @@ let ise_array2 evd f v1 v2 = let rec evar_conv_x env evd pbty term1 term2 = let sigma = evars_of evd in - let term1 = apprec_nohdbeta env evd (whd_castappevar sigma term1) in - let term2 = apprec_nohdbeta env evd (whd_castappevar sigma term2) in + let term1 = whd_castappevar sigma term1 in + let term2 = whd_castappevar sigma term2 in (* 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 then - (evd,true) - else if is_undefined_evar evd term1 then + is_fconv pbty env (evars_of evd) term1 term2 + then + (evd,true) + else + let term1 = apprec_nohdbeta env evd term1 in + let term2 = apprec_nohdbeta env evd term2 in + if is_undefined_evar evd term1 then solve_simple_eqn evar_conv_x env evd (pbty,destEvar term1,term2) else if is_undefined_evar evd term2 then solve_simple_eqn evar_conv_x env evd (pbty,destEvar term2,term1) |