diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-23 17:30:03 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-23 17:30:03 +0000 |
| commit | fe0bf68ccfe9ab635012b8e396011d20e8c25612 (patch) | |
| tree | 7f96682cda2b159ad26a198b72cdd5dd4b1f5c10 /pretyping | |
| parent | 68259c3088f9ad830a9dab4ae495000ab2646ffc (diff) | |
reparation des contribs: lors de l'unification, reduire les beta redexes
avant d'expanser les constantes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3604 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 289a80ced..623d0e99d 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -218,7 +218,14 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = with Not_found -> check_conv_record appr2 appr1) with _ -> false) and f4 () = - match eval_flexible_term env flex2 with + (* heuristic: unfold second argument first, exception made + if the first argument is a beta-redex (expand a constant + only if necessary) *) + let val2 = + match kind_of_term flex1 with + Lambda _ -> None + | _ -> eval_flexible_term env flex2 in + match val2 with | Some v2 -> evar_eqappr_x env isevars pbty appr1 (evar_apprec env isevars l2 v2) |