diff options
Diffstat (limited to 'vernac/comInductive.ml')
| -rw-r--r-- | vernac/comInductive.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 790e83dbef..b93e8d9ac8 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -27,7 +27,6 @@ open Impargs open Reductionops open Indtypes open Pretyping -open Evarutil open Indschemes open Context.Rel.Declaration open Entries @@ -158,7 +157,7 @@ let sign_level env evd sign = | LocalDef _ -> lev, push_rel d env | LocalAssum _ -> let s = destSort (Reduction.whd_all env - (EConstr.Unsafe.to_constr (nf_evar evd (Retyping.get_type_of env evd (EConstr.of_constr (RelDecl.get_type d)))))) + (EConstr.to_constr 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)) @@ -333,7 +332,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = List.iter check_param paramsl; let env0 = Global.env() in let pl = (List.hd indl).ind_univs in - let sigma, decl = Univdecls.interp_univ_decl_opt env0 pl in + let sigma, decl = interp_univ_decl_opt env0 pl in let sigma, (impls, ((env_params, ctx_params), userimpls)) = interp_context_evars env0 sigma paramsl in |