diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/entries.ml (renamed from kernel/entries.mli) | 0 | ||||
| -rw-r--r-- | kernel/kernel.mllib | 5 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 4 | ||||
| -rw-r--r-- | kernel/univ.ml | 8 | ||||
| -rw-r--r-- | kernel/univ.mli | 6 |
5 files changed, 3 insertions, 20 deletions
diff --git a/kernel/entries.mli b/kernel/entries.ml index 3fa25c142a..3fa25c142a 100644 --- a/kernel/entries.mli +++ b/kernel/entries.ml diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 0813315b5b..9946348541 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -13,9 +13,11 @@ Mod_subst Cbytecodes Copcodes Cemitcodes +Opaqueproof +Declarations +Entries Nativevalues Primitives -Opaqueproof Declareops Retroknowledge Conv_oracle @@ -41,5 +43,4 @@ Nativelibrary Safe_typing Vm Csymtable -Declarations Vconv diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 3e516cae04..cf82d54ec1 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -265,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 @@ -299,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 diff --git a/kernel/univ.ml b/kernel/univ.ml index 6614d60276..02b02db893 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1292,14 +1292,6 @@ let subst_univs_constraints subst csts = (fun c cstrs -> subst_univs_constraint subst c cstrs) csts Constraint.empty -(** Substitute instance inst for ctx in csts *) -let instantiate_univ_context (ctx, csts) = - (ctx, subst_instance_constraints ctx csts) - -(** Substitute instance inst for ctx in universe constraints and subtyping constraints *) -let instantiate_cumulativity_info (univcst, subtpcst) = - (instantiate_univ_context univcst, instantiate_univ_context subtpcst) - let make_instance_subst i = let arr = Instance.to_array i in Array.fold_left_i (fun i acc l -> diff --git a/kernel/univ.mli b/kernel/univ.mli index 53297ac462..99092a543e 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -461,12 +461,6 @@ val abstract_cumulativity_info : cumulativity_info -> universe_level_subst * abs val make_abstract_instance : abstract_universe_context -> universe_instance -(** Don't use. *) -val instantiate_univ_context : abstract_universe_context -> universe_context - -(** Don't use. *) -val instantiate_cumulativity_info : abstract_cumulativity_info -> cumulativity_info - (** {6 Pretty-printing of universes. } *) val pr_constraint_type : constraint_type -> Pp.std_ppcmds |