diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 4 | ||||
| -rw-r--r-- | toplevel/indschemes.ml | 2 | ||||
| -rw-r--r-- | toplevel/record.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
4 files changed, 5 insertions, 5 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 249d41845..14a45f837 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 c + | None -> 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 (RelDecl.get_type d)))) + (nf_evar evd (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)) diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 3f818f960..fef99d8af 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -403,7 +403,7 @@ let do_mutual_induction_scheme lnamedepindsort = in let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in let declare decl fi lrecref = - let decltype = Retyping.get_type_of env0 sigma decl in + let decltype = Retyping.get_type_of env0 sigma (EConstr.of_constr decl) in let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in let cst = define fi UserIndividualRequest sigma proof_output (Some decltype) in ConstRef cst :: lrecref diff --git a/toplevel/record.ml b/toplevel/record.ml index ffe7980ef..5f2b99f90 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -84,7 +84,7 @@ let compute_constructor_level evars env l = List.fold_right (fun d (env, univ) -> let univ = if is_local_assum d then - let s = Retyping.get_sort_of env evars (RelDecl.get_type d) in + let s = Retyping.get_sort_of env evars (EConstr.of_constr (RelDecl.get_type d)) in Univ.sup (univ_of_sort s) univ else univ in (push_rel d env, univ)) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 593aa9578..c39b4dc25 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1579,7 +1579,7 @@ let vernac_check_may_eval redexp glopt rc = let c = nf c in let j = if Evarutil.has_undefined_evars sigma' c then - Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c) + Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' (EConstr.of_constr c)) else (* OK to call kernel which does not support evars *) Arguments_renaming.rename_typing env c in |