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/extraction | |
| 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/extraction')
| -rw-r--r-- | contrib/extraction/extraction.ml | 3 |
1 files changed, 2 insertions, 1 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 |