diff options
| author | herbelin | 2006-04-28 12:24:14 +0000 |
|---|---|---|
| committer | herbelin | 2006-04-28 12:24:14 +0000 |
| commit | a184d54b95c40bc2890fc91f236bbdf983ebc83d (patch) | |
| tree | d95ef613b68e96c0e7de041baae4c721bd48cd25 /pretyping/reductionops.ml | |
| parent | 11aaf97fa5f773c8a81d12255414cd3f5d189d25 (diff) | |
Standardisation du nom des méthodes de Evd
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8759 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 20b48a01ae..9a01250250 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -428,13 +428,13 @@ let whd_betadeltaiota_nolet env sigma x = let rec whd_evar sigma c = match kind_of_term c with | Evar (ev,args) - when Evd.in_dom sigma ev & Evd.is_defined sigma ev -> + when Evd.mem sigma ev & Evd.is_defined sigma ev -> whd_evar sigma (Evd.existential_value sigma (ev,args)) | Sort s when is_sort_variable sigma s -> whd_sort_variable sigma c | _ -> collapse_appl c -let nf_evar evd = - local_strong (whd_evar evd) +let nf_evar sigma = + local_strong (whd_evar sigma) (* lazy reduction functions. The infos must be created for each term *) let clos_norm_flags flgs env sigma t = |