diff options
| author | herbelin | 2001-07-02 22:31:43 +0000 |
|---|---|---|
| committer | herbelin | 2001-07-02 22:31:43 +0000 |
| commit | 9df7ef3bdd8288cb06888b7390441eae8d2c7aba (patch) | |
| tree | f98f182862cd74eba63db25ab44dcfebc27339e9 /contrib | |
| parent | c25b393a7e121d2742375a3fb00776e5fb9d79da (diff) | |
Nettoyage/restructuration des ensembles d'indicateurs de réductions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1819 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/extraction/extraction.ml | 3 | ||||
| -rw-r--r-- | contrib/ring/ring.ml | 6 |
2 files changed, 6 insertions, 3 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 2b0f93b0e3..0000b26a18 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -101,7 +101,8 @@ let none = Evd.empty let type_of env c = Typing.type_of env Evd.empty (strip_outer_cast c) -let whd_betaiotalet = clos_norm_flags (UNIFORM, red_add betaiota_red ZETA) +open RedFlags +let whd_betaiotalet = clos_norm_flags (UNIFORM, mkflags [fBETA;fIOTA;fZETA]) let is_axiom sp = (Global.lookup_constant sp).const_body = None diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index a326a7a18c..0a70426ea5 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -548,13 +548,15 @@ let constants_to_unfold = (* SectionPathSet.empty *) (* Unfolds the functions interp and find_btree in the term c of goal gl *) +open RedFlags let polynom_unfold_tac = - let flags = (UNIFORM, red_add betaiota_red (CONST constants_to_unfold)) in + let flags = + (UNIFORM, mkflags(fBETA::fIOTA::fEVAR::(List.map fCONST constants_to_unfold))) in reduct_in_concl (cbv_norm_flags flags) let polynom_unfold_tac_in_term gl = let flags = - (UNIFORM, red_add betaiotazeta_red (CONST constants_to_unfold)) + (UNIFORM,mkflags(fBETA::fIOTA::fEVAR::fZETA::(List.map fCONST constants_to_unfold))) in cbv_norm_flags flags (pf_env gl) (project gl) |