diff options
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 13 |
1 files changed, 4 insertions, 9 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 5370bcea43..cf82d54ec1 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -131,8 +131,7 @@ let inline_side_effects env body ctx side_eff = (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args) | Polymorphic_const auctx -> (** Inline the term to emulate universe polymorphism *) - let data = (Univ.AUContext.instance auctx, b) in - let subst = Cmap_env.add c (Inl data) subst in + let subst = Cmap_env.add c (Inl b) subst in (subst, var, ctx, args) in let (subst, len, ctx, args) = List.fold_left fold (Cmap_env.empty, 1, ctx, []) side_eff in @@ -142,7 +141,7 @@ let inline_side_effects env body ctx side_eff = let data = try Some (Cmap_env.find c subst) with Not_found -> None in begin match data with | None -> t - | Some (Inl (inst, b)) -> + | Some (Inl b) -> (** [b] is closed but may refer to other constants *) subst_const i k (Vars.subst_instance_constr u b) | Some (Inr n) -> @@ -266,11 +265,8 @@ let infer_declaration ~trust env kn dcl = let body,env,ectx = skip_trusted_seff valid_signatures body env in let j = infer env body in unzip ectx j in - let subst = Univ.LMap.empty in let _ = judge_of_cast env j DEFAULTcast tyj in - assert (eq_constr typ tyj.utj_val); let c = hcons_constr j.uj_val in - let _typ = RegularArity (Vars.subst_univs_level_constr subst typ) in feedback_completion_typecheck feedback_id; c, uctx) in let def = OpaqueDef (Opaqueproof.create proofterm) in @@ -300,7 +296,6 @@ let infer_declaration ~trust env kn dcl = | Some t -> let tj = infer_type env t in let _ = judge_of_cast env j DEFAULTcast tj in - assert (eq_constr t tj.utj_val); RegularArity (Vars.subst_univs_level_constr usubst t) in let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in @@ -470,7 +465,7 @@ let constant_entry_of_side_effect cb u = match cb.const_universes with | Monomorphic_const ctx -> false, ctx | Polymorphic_const auctx -> - true, Univ.instantiate_univ_context auctx + true, Univ.AUContext.repr auctx in let pt = match cb.const_body, u with |