diff options
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/decl_interp.ml | 4 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 8 |
2 files changed, 6 insertions, 6 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 10c09c8d6b..a862423e99 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -153,8 +153,8 @@ 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.all env in - (fun t -> Closure.whd_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos CClosure.all env in + (fun t -> CClosure.whd_val infos (CClosure.inject t)) let _eq = lazy (Universes.constr_of_global (Coqlib.glob_eq)) diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 5ed426c1df..97c9d5f4a2 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -84,12 +84,12 @@ let tcl_erase_info gls = tcl_change_info_gen info_gen gls let special_whd gl= - let infos=Closure.create_clos_infos Closure.all (pf_env gl) in - (fun t -> Closure.whd_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos CClosure.all (pf_env gl) in + (fun t -> CClosure.whd_val infos (CClosure.inject t)) let special_nf gl= - let infos=Closure.create_clos_infos Closure.betaiotazeta (pf_env gl) in - (fun t -> Closure.norm_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos CClosure.betaiotazeta (pf_env gl) in + (fun t -> CClosure.norm_val infos (CClosure.inject t)) let is_good_inductive env ind = let mib,oib = Inductive.lookup_mind_specif env ind in |