diff options
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 |