diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-19 13:41:20 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-19 13:41:20 +0000 |
| commit | cad1432683f0fa93efaf64f26803a44f64fd1bd0 (patch) | |
| tree | d79fae7b07bc06fb366f1d02e66cf1891b4bf7e3 /pretyping | |
| parent | 4cb5880d9f3afa0b92eeb49a1295341da3769f81 (diff) | |
Retour en arrière pour raison de compatibilité sur la suppression du nf_evar
dans clos_norm_flags (cf échec dans CoRN.Transc.InvTrigonom.Tan_ilim). Ceci
dit :
- cela ne me parait pas moral que clos_norm_flags s'occupe de
normaliser les evars,
- mais comme "evar" n'est pas un flag supporté par closure.ml, on ne
peut pas le donner à la demande comme argument de clos_norm_flags
(question: pourrait-on faire supporter la réduction Evar par closure.ml ??).
Plus généralement, il y a un problème avec la propagation des
instantiations des evars à travers les buts (cf lemme eapply_evar dans
test-suite/success/apply.v).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11470 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/reductionops.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index e3553ddd6..7fdcded00 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -517,8 +517,10 @@ let nf_evar sigma = local_strong (whd_evar sigma) (* lazy reduction functions. The infos must be created for each term *) +(* Note by HH [oct 08] : why would it be the job of clos_norm_flags to add + a [nf_evar] here *) let clos_norm_flags flgs env sigma t = - norm_val (create_clos_infos flgs env) (inject ((*nf_evar sigma *)t)) + norm_val (create_clos_infos flgs env) (inject (nf_evar sigma t)) let nf_beta = clos_norm_flags Closure.beta empty_env Evd.empty let nf_betaiota = clos_norm_flags Closure.betaiota empty_env Evd.empty |