diff options
Diffstat (limited to 'plugins/decl_mode/decl_interp.ml')
| -rw-r--r-- | plugins/decl_mode/decl_interp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 34307a358..c0ef34305 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -153,7 +153,7 @@ let interp_constr check_sort env sigma c = fst (understand env sigma (fst c)) let special_whd env = - let infos=Closure.create_clos_infos Closure.betadeltaiota env in + let infos=Closure.create_clos_infos Closure.all env in (fun t -> Closure.whd_val infos (Closure.inject t)) let _eq = lazy (Universes.constr_of_global (Coqlib.glob_eq)) |