diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-12 15:44:01 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-12 15:44:01 +0000 |
| commit | c13a9b5eb6479cbd35b90516e623b0a41ad22667 (patch) | |
| tree | 3b6500ba67e3fd3fa55e9a2b7c8dfb629cc87e49 /pretyping/evarconv.ml | |
| parent | 18312d873c5d68c37cceb7388200f3567f459146 (diff) | |
evar reduction is already made by whd_*
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15615 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index a01140795..871e676a2 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -57,14 +57,7 @@ let eval_flexible_term ts env c = | _ -> assert false let evar_apprec ts env evd stack c = - let sigma = evd in - let rec aux s = - let (t,stack) = whd_betaiota_deltazeta_for_iota_state ts env sigma s in - match kind_of_term t with - | Evar (evk,_ as ev) when Evd.is_defined sigma evk -> - aux (Evd.existential_value sigma ev, stack) - | _ -> decompose_app (zip (t, stack)) - in aux (c, append_stack_app_list stack empty_stack) + decompose_app (zip (whd_betaiota_deltazeta_for_iota_state ts env evd (c,append_stack_app_list stack empty_stack))) let apprec_nohdbeta ts env evd c = match kind_of_term (fst (Reductionops.whd_stack evd c)) with |