diff options
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 820c1b885..1fc89b8b0 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -206,7 +206,7 @@ let do_definition ident k pl bl red_option c ctypopt hook = assert(Univ.ContextSet.is_empty ctx); let typ = match ce.const_entry_type with | Some t -> t - | None -> Retyping.get_type_of env evd (EConstr.of_constr c) + | None -> EConstr.Unsafe.to_constr (Retyping.get_type_of env evd (EConstr.of_constr c)) in Obligations.check_evars env evd; let obls, _, c, cty = @@ -459,7 +459,7 @@ let sign_level env evd sign = | LocalDef _ -> lev, push_rel d env | LocalAssum _ -> let s = destSort (Reduction.whd_all env - (nf_evar evd (Retyping.get_type_of env evd (EConstr.of_constr (RelDecl.get_type d))))) + (nf_evar evd (EConstr.Unsafe.to_constr (Retyping.get_type_of env evd (EConstr.of_constr (RelDecl.get_type d)))))) in let u = univ_of_sort s in (Univ.sup u lev, push_rel d env)) @@ -1106,6 +1106,7 @@ let interp_recursive isfix fixl notations = (fun env' id t -> if Flags.is_program_mode () then let sort = Evarutil.evd_comb1 (Typing.type_of ~refresh:true env) evdref (EConstr.of_constr t) in + let sort = EConstr.Unsafe.to_constr sort in let fixprot = try let app = mkApp (delayed_force fix_proto, [|sort; t|]) in |