diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-02-09 15:58:32 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-02-09 15:58:32 +0000 |
| commit | c580f69cc36cc4cc908febb900a55ae751039a0c (patch) | |
| tree | 17a176851279624a58a2a75ca1dea071ec78bcca /pretyping/evarconv.ml | |
| parent | 6160f53e89800a785d773c4130b08fbe7c345651 (diff) | |
memoized is_ground_env
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11893 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 31 |
1 files changed, 19 insertions, 12 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index aba6e2e19..d7da100ab 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -164,18 +164,25 @@ 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_ground_env evd env - then (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 - 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) - else - evar_eqappr_x env evd pbty (decompose_app term1) (decompose_app term2) + let ground_test = + if is_ground_term evd term1 && is_ground_term evd term2 then + if is_fconv pbty env (evars_of evd) term1 term2 then + Some true + else if is_ground_env evd env then Some false + else None + else None in + match ground_test with + Some b -> (evd,b) + | None -> + 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) + else + evar_eqappr_x env evd pbty + (decompose_app term1) (decompose_app term2) and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = (* Evar must be undefined since we have whd_ised *) |