aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cClosure.ml2
-rw-r--r--kernel/cooking.ml54
-rw-r--r--kernel/entries.ml7
-rw-r--r--kernel/indtypes.ml10
-rw-r--r--kernel/inductive.ml4
-rw-r--r--kernel/mod_typing.ml4
-rw-r--r--kernel/nativelambda.ml2
-rw-r--r--kernel/opaqueproof.ml2
-rw-r--r--kernel/opaqueproof.mli2
-rw-r--r--kernel/safe_typing.ml19
-rw-r--r--kernel/safe_typing.mli2
-rw-r--r--kernel/subtyping.ml2
-rw-r--r--kernel/term_typing.ml51
-rw-r--r--kernel/term_typing.mli6
-rw-r--r--kernel/univ.ml34
-rw-r--r--kernel/univ.mli13
-rw-r--r--kernel/vars.ml43
-rw-r--r--kernel/vars.mli6
18 files changed, 99 insertions, 164 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 31ded9129a..11616da7b3 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -810,7 +810,7 @@ let eta_expand_ind_stack env ind m s (f, s') =
let mib = lookup_mind (fst ind) env in
match mib.Declarations.mind_record with
| Some (Some (_,projs,pbs)) when
- mib.Declarations.mind_finite == Decl_kinds.BiFinite ->
+ mib.Declarations.mind_finite == Declarations.BiFinite ->
(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
let pars = mib.Declarations.mind_nparams in
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 7b921d35be..23a578d993 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -168,38 +168,47 @@ let on_body ml hy f = function
{ Opaqueproof.modlist = ml; abstract = hy } o)
let expmod_constr_subst cache modlist subst c =
+ let subst = Univ.make_instance_subst subst in
let c = expmod_constr cache modlist c in
Vars.subst_univs_level_constr subst c
-let cook_constr { Opaqueproof.modlist ; abstract } c =
+let cook_constr { Opaqueproof.modlist ; abstract = (vars, subst, _) } c =
let cache = RefTable.create 13 in
- let expmod = expmod_constr_subst cache modlist (pi2 abstract) in
- let hyps = Context.Named.map expmod (pi1 abstract) in
+ let expmod = expmod_constr_subst cache modlist subst in
+ let hyps = Context.Named.map expmod vars in
abstract_constant_body (expmod c) hyps
-let lift_univs cb subst =
+let lift_univs cb subst auctx0 =
match cb.const_universes with
- | Monomorphic_const ctx -> subst, (Monomorphic_const ctx)
- | Polymorphic_const auctx ->
- if (Univ.LMap.is_empty subst) then
- subst, (Polymorphic_const auctx)
+ | Monomorphic_const ctx ->
+ assert (AUContext.is_empty auctx0);
+ subst, (Monomorphic_const ctx)
+ | Polymorphic_const auctx ->
+ (** Given a named instance [subst := u₀ ... uₙ₋₁] together with an abstract
+ context [auctx0 := 0 ... n - 1 |= C{0, ..., n - 1}] of the same length,
+ and another abstract context relative to the former context
+ [auctx := 0 ... m - 1 |= C'{u₀, ..., uₙ₋₁, 0, ..., m - 1}],
+ construct the lifted abstract universe context
+ [0 ... n - 1 n ... n + m - 1 |=
+ C{0, ... n - 1} ∪
+ C'{0, ..., n - 1, n, ..., n + m - 1} ]
+ together with the instance
+ [u₀ ... uₙ₋₁ Var(0) ... Var (m - 1)].
+ *)
+ if (Univ.Instance.is_empty subst) then
+ (** Still need to take the union for the constraints between globals *)
+ subst, (Polymorphic_const (AUContext.union auctx0 auctx))
else
- let len = Univ.LMap.cardinal subst in
- let rec gen_subst i acc =
- if i < 0 then acc
- else
- let acc = Univ.LMap.add (Level.var i) (Level.var (i + len)) acc in
- gen_subst (pred i) acc
- in
- let subst = gen_subst (Univ.AUContext.size auctx - 1) subst in
- let auctx' = Univ.subst_univs_level_abstract_universe_context subst auctx in
- subst, (Polymorphic_const auctx')
+ let ainst = Univ.make_abstract_instance auctx in
+ let subst = Instance.append subst ainst in
+ let auctx' = Univ.subst_univs_level_abstract_universe_context (Univ.make_instance_subst subst) auctx in
+ subst, (Polymorphic_const (AUContext.union auctx0 auctx'))
let cook_constant ~hcons env { from = cb; info } =
let { Opaqueproof.modlist; abstract } = info in
let cache = RefTable.create 13 in
let abstract, usubst, abs_ctx = abstract in
- let usubst, univs = lift_univs cb usubst in
+ let usubst, univs = lift_univs cb usubst abs_ctx in
let expmod = expmod_constr_subst cache modlist usubst in
let hyps = Context.Named.map expmod abstract in
let map c =
@@ -234,13 +243,6 @@ let cook_constant ~hcons env { from = cb; info } =
proj_eta = etab, etat;
proj_type = ty'; proj_body = c' }
in
- let univs =
- match univs with
- | Monomorphic_const ctx ->
- assert (AUContext.is_empty abs_ctx); univs
- | Polymorphic_const auctx ->
- Polymorphic_const (AUContext.union abs_ctx auctx)
- in
{
cook_body = body;
cook_type = typ;
diff --git a/kernel/entries.ml b/kernel/entries.ml
index ca79de404d..36b75668b2 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -81,6 +81,13 @@ type 'a definition_entry = {
const_entry_opaque : bool;
const_entry_inline_code : bool }
+type section_def_entry = {
+ secdef_body : constr;
+ secdef_secctx : Context.Named.t option;
+ secdef_feedback : Stateid.t option;
+ secdef_type : types option;
+}
+
type inline = int option (* inlining level, None for no inlining *)
type parameter_entry =
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 8e9b606a58..b117f8714b 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -710,7 +710,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
best-effort fashion. *)
let check_positivity ~chkpos kn env_ar_par paramsctxt finite inds =
let ntypes = Array.length inds in
- let recursive = finite != Decl_kinds.BiFinite in
+ let recursive = finite != BiFinite in
let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in
let ra_env_ar = Array.rev_to_list rc in
let nparamsctxt = Context.Rel.length paramsctxt in
@@ -879,9 +879,13 @@ let abstract_inductive_universes iu =
match iu with
| Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx)
| Polymorphic_ind_entry ctx ->
- let (inst, auctx) = Univ.abstract_universes ctx in (inst, Polymorphic_ind auctx)
+ let (inst, auctx) = Univ.abstract_universes ctx in
+ let inst = Univ.make_instance_subst inst in
+ (inst, Polymorphic_ind auctx)
| Cumulative_ind_entry cumi ->
- let (inst, acumi) = Univ.abstract_cumulativity_info cumi in (inst, Cumulative_ind acumi)
+ let (inst, acumi) = Univ.abstract_cumulativity_info cumi in
+ let inst = Univ.make_instance_subst inst in
+ (inst, Cumulative_ind acumi)
let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr recargs =
let ntypes = Array.length inds in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 2a629f00a9..28a09b81b0 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -38,14 +38,14 @@ let find_inductive env c =
let (t, l) = decompose_app (whd_all env c) in
match kind t with
| Ind ind
- when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite <> Decl_kinds.CoFinite -> (ind, l)
+ when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite <> CoFinite -> (ind, l)
| _ -> raise Not_found
let find_coinductive env c =
let (t, l) = decompose_app (whd_all env c) in
match kind t with
| Ind ind
- when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite == Decl_kinds.CoFinite -> (ind, l)
+ when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite == CoFinite -> (ind, l)
| _ -> raise Not_found
let inductive_params (mib,_) = mib.mind_nparams
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index f7e755f005..b7eb481ee3 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -94,8 +94,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
let ctx = Univ.ContextSet.of_context ctx in
c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst ctx
| Polymorphic_const uctx ->
- let subst, ctx = Univ.abstract_universes ctx in
- let c = Vars.subst_univs_level_constr subst c in
+ let inst, ctx = Univ.abstract_universes ctx in
+ let c = Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in
let () =
if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then
error_incorrect_with_constraint lab
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index de4dc21079..160a90dc2f 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -515,7 +515,7 @@ let rec lambda_of_constr env sigma c =
{ asw_ind = ind;
asw_ci = ci;
asw_reloc = tbl;
- asw_finite = mib.mind_finite <> Decl_kinds.CoFinite;
+ asw_finite = mib.mind_finite <> CoFinite;
asw_prefix = prefix}
in
(* translation of the argument *)
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 45a62d55a1..c2fcfbfd6a 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -16,7 +16,7 @@ type work_list = (Instance.t * Id.t array) Cmap.t *
type cooking_info = {
modlist : work_list;
- abstract : Context.Named.t * Univ.universe_level_subst * Univ.AUContext.t }
+ abstract : Context.Named.t * Univ.Instance.t * Univ.AUContext.t }
type proofterm = (constr * Univ.ContextSet.t) Future.computation
type opaque =
| Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 20d76ce238..c8339e6eb3 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -49,7 +49,7 @@ type work_list = (Univ.Instance.t * Id.t array) Cmap.t *
type cooking_info = {
modlist : work_list;
- abstract : Context.Named.t * Univ.universe_level_subst * Univ.AUContext.t }
+ abstract : Context.Named.t * Univ.Instance.t * Univ.AUContext.t }
(* The type has two caveats:
1) cook_constr is defined after
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index fa984515a7..93b8e278fa 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -382,22 +382,9 @@ let safe_push_named d env =
let push_named_def (id,de) senv =
- let open Entries in
- let c,typ,univs = Term_typing.translate_local_def senv.env id de in
- let poly = match de.Entries.const_entry_universes with
- | Monomorphic_const_entry _ -> false
- | Polymorphic_const_entry _ -> true
- in
- let c, univs = match c with
- | Def c -> Mod_subst.force_constr c, univs
- | OpaqueDef o ->
- Opaqueproof.force_proof (Environ.opaque_tables senv.env) o,
- Univ.ContextSet.union univs
- (Opaqueproof.force_constraints (Environ.opaque_tables senv.env) o)
- | _ -> assert false in
- let senv' = push_context_set poly univs senv in
- let env'' = safe_push_named (LocalDef (id,c,typ)) senv'.env in
- univs, {senv' with env=env''}
+ let c, typ = Term_typing.translate_local_def senv.env id de in
+ let env'' = safe_push_named (LocalDef (id, c, typ)) senv.env in
+ { senv with env = env'' }
let push_named_assum ((id,t,poly),ctx) senv =
let senv' = push_context_set poly ctx senv in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index fbc398a2aa..757b803a39 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -90,7 +90,7 @@ val push_named_assum :
(** Returns the full universe context necessary to typecheck the definition
(futures are forced) *)
val push_named_def :
- Id.t * unit Entries.definition_entry -> Univ.ContextSet.t safe_transformer
+ Id.t * Entries.section_def_entry -> safe_transformer0
(** Insertion of global axioms or definitions *)
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 2913c6dfad..d0d5cb1d56 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -193,7 +193,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
(arities_of_specif (mind, inst) (mib2, p2))
in
let check f test why = if not (test (f mib1) (f mib2)) then error (why (f mib2)) in
- check (fun mib -> mib.mind_finite<>Decl_kinds.CoFinite) (==) (fun x -> FiniteInductiveFieldExpected x);
+ check (fun mib -> mib.mind_finite<>CoFinite) (==) (fun x -> FiniteInductiveFieldExpected x);
check (fun mib -> mib.mind_ntypes) Int.equal (fun x -> InductiveNumbersFieldExpected x);
assert (List.is_empty mib1.mind_hyps && List.is_empty mib2.mind_hyps);
assert (Array.length mib1.mind_packets >= 1
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 761eab511a..cbc4ee2ec4 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -227,17 +227,15 @@ let feedback_completion_typecheck =
Option.iter (fun state_id ->
feedback ~id:state_id Feedback.Complete)
-let abstract_constant_universes abstract = function
+let abstract_constant_universes = function
| Monomorphic_const_entry uctx ->
Univ.empty_level_subst, Monomorphic_const uctx
| Polymorphic_const_entry uctx ->
- if not abstract then
- Univ.empty_level_subst, Monomorphic_const (Univ.ContextSet.of_context uctx)
- else
- let sbst, auctx = Univ.abstract_universes uctx in
- sbst, Polymorphic_const auctx
+ let sbst, auctx = Univ.abstract_universes uctx in
+ let sbst = Univ.make_instance_subst sbst in
+ sbst, Polymorphic_const auctx
-let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry) =
+let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
match dcl with
| ParameterEntry (ctx,(t,uctx),nl) ->
let env = match uctx with
@@ -245,10 +243,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
| Polymorphic_const_entry uctx -> push_context ~strict:false uctx env
in
let j = infer env t in
- let abstract = not (Option.is_empty kn) in
- let usubst, univs =
- abstract_constant_universes abstract uctx
- in
+ let usubst, univs = abstract_constant_universes uctx in
let c = Typeops.assumption_of_judgment env j in
let t = Constr.hcons (Vars.subst_univs_level_constr usubst c) in
{
@@ -316,12 +311,11 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
| SideEffects _ -> inline_side_effects env body ctx side_eff
in
let env = push_context_set ~strict:(not poly) ctx env in
- let abstract = not (Option.is_empty kn) in
let ctx = if poly
then Polymorphic_const_entry (Univ.ContextSet.to_context ctx)
else Monomorphic_const_entry ctx
in
- let usubst, univs = abstract_constant_universes abstract ctx in
+ let usubst, univs = abstract_constant_universes ctx in
let j = infer env body in
let typ = match typ with
| None ->
@@ -493,7 +487,7 @@ let build_constant_declaration kn env result =
let translate_constant mb env kn ce =
build_constant_declaration kn env
- (infer_declaration ~trust:mb env (Some kn) ce)
+ (infer_declaration ~trust:mb env ce)
let constant_entry_of_side_effect cb u =
let univs =
@@ -607,7 +601,17 @@ let translate_recipe env kn r =
let translate_local_def env id centry =
let open Cooking in
- let decl = infer_declaration ~trust:Pure env None (DefinitionEntry centry) in
+ let body = Future.from_val ((centry.secdef_body, Univ.ContextSet.empty), ()) in
+ let centry = {
+ const_entry_body = body;
+ const_entry_secctx = centry.secdef_secctx;
+ const_entry_feedback = centry.secdef_feedback;
+ const_entry_type = centry.secdef_type;
+ const_entry_universes = Monomorphic_const_entry Univ.ContextSet.empty;
+ const_entry_opaque = false;
+ const_entry_inline_code = false;
+ } in
+ let decl = infer_declaration ~trust:Pure env (DefinitionEntry centry) in
let typ = decl.cook_type in
if Option.is_empty decl.cook_context && !Flags.record_aux_file then begin
match decl.cook_body with
@@ -619,11 +623,22 @@ let translate_local_def env id centry =
(Opaqueproof.force_proof (opaque_tables env) lc) in
record_aux env ids_typ ids_def
end;
- let univs = match decl.cook_universes with
- | Monomorphic_const ctx -> ctx
+ let () = match decl.cook_universes with
+ | Monomorphic_const ctx -> assert (Univ.ContextSet.is_empty ctx)
| Polymorphic_const _ -> assert false
in
- decl.cook_body, typ, univs
+ let c = match decl.cook_body with
+ | Def c -> Mod_subst.force_constr c
+ | OpaqueDef o ->
+ let p = Opaqueproof.force_proof (Environ.opaque_tables env) o in
+ let cst = Opaqueproof.force_constraints (Environ.opaque_tables env) o in
+ (** Let definitions are ensured to have no extra constraints coming from
+ the body by virtue of the typing of [Entries.section_def_entry]. *)
+ let () = assert (Univ.ContextSet.is_empty cst) in
+ p
+ | Undef _ -> assert false
+ in
+ c, typ
(* Insertion of inductive types. *)
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index c771452a19..7bc029010f 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -18,8 +18,8 @@ type _ trust =
| Pure : unit trust
| SideEffects : structure_body -> side_effects trust
-val translate_local_def : env -> Id.t -> unit definition_entry ->
- constant_def * types * Univ.ContextSet.t
+val translate_local_def : env -> Id.t -> section_def_entry ->
+ constr * types
val translate_local_assum : env -> types -> types
@@ -72,7 +72,7 @@ val translate_recipe : env -> Constant.t -> Cooking.recipe -> constant_body
(** Internal functions, mentioned here for debug purpose only *)
-val infer_declaration : trust:'a trust -> env -> Constant.t option ->
+val infer_declaration : trust:'a trust -> env ->
'a constant_entry -> Cooking.result
val build_constant_declaration :
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 8cf9028fb1..f72f6f26a9 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -686,12 +686,6 @@ let enforce_leq u v c =
let enforce_leq_level u v c =
if Level.equal u v then c else Constraint.add (u,Le,v) c
-let enforce_univ_constraint (u,d,v) =
- match d with
- | Eq -> enforce_eq u v
- | Le -> enforce_leq u v
- | Lt -> enforce_leq (super u) v
-
(* Miscellaneous functions to remove or test local univ assumed to
occur in a universe *)
@@ -718,14 +712,6 @@ type universe_level_subst = universe_level universe_map
(** A full substitution might involve algebraic universes *)
type universe_subst = universe universe_map
-let level_subst_of f =
- fun l ->
- try let u = f l in
- match Universe.level u with
- | None -> l
- | Some l -> l
- with Not_found -> l
-
module Instance : sig
type t = Level.t array
@@ -1128,24 +1114,6 @@ let subst_univs_universe fn ul =
List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.tip u))
substs nosubst
-let subst_univs_level fn l =
- try Some (fn l)
- with Not_found -> None
-
-let subst_univs_constraint fn (u,d,v as c) cstrs =
- let u' = subst_univs_level fn u in
- let v' = subst_univs_level fn v in
- match u', v' with
- | None, None -> Constraint.add c cstrs
- | Some u, None -> enforce_univ_constraint (u,d,make v) cstrs
- | None, Some v -> enforce_univ_constraint (make u,d,v) cstrs
- | Some u, Some v -> enforce_univ_constraint (u,d,v) cstrs
-
-let subst_univs_constraints subst csts =
- Constraint.fold
- (fun c cstrs -> subst_univs_constraint subst c cstrs)
- csts Constraint.empty
-
let make_instance_subst i =
let arr = Instance.to_array i in
Array.fold_left_i (fun i acc l ->
@@ -1168,7 +1136,7 @@ let abstract_universes ctx =
(UContext.constraints ctx)
in
let ctx = UContext.make (instance, cstrs) in
- subst, ctx
+ instance, ctx
let abstract_cumulativity_info (univcst, substcst) =
let instance, univcst = abstract_universes univcst in
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 4593944395..63bef1b81b 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -238,8 +238,6 @@ type universe_level_subst_fn = Level.t -> Level.t
type universe_subst = Universe.t universe_map
type universe_level_subst = Level.t universe_map
-val level_subst_of : universe_subst_fn -> universe_level_subst_fn
-
(** {6 Universe instances} *)
module Instance :
@@ -461,18 +459,21 @@ val is_empty_subst : universe_subst -> bool
val make_subst : universe_subst -> universe_subst_fn
val subst_univs_universe : universe_subst_fn -> Universe.t -> Universe.t
-val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t
+(** Only user in the kernel is template polymorphism. Ideally we get rid of
+ this code if it goes away. *)
(** Substitution of instances *)
val subst_instance_instance : Instance.t -> Instance.t -> Instance.t
val subst_instance_universe : Instance.t -> Universe.t -> Universe.t
val make_instance_subst : Instance.t -> universe_level_subst
-val make_inverse_instance_subst : Instance.t -> universe_level_subst
+(** Creates [u(0) ↦ 0; ...; u(n-1) ↦ n - 1] out of [u(0); ...; u(n - 1)] *)
-val abstract_universes : UContext.t -> universe_level_subst * AUContext.t
+val make_inverse_instance_subst : Instance.t -> universe_level_subst
-val abstract_cumulativity_info : CumulativityInfo.t -> universe_level_subst * ACumulativityInfo.t
+val abstract_universes : UContext.t -> Instance.t * AUContext.t
+val abstract_cumulativity_info : CumulativityInfo.t -> Instance.t * ACumulativityInfo.t
+(** TODO: move universe abstraction out of the kernel *)
val make_abstract_instance : AUContext.t -> Instance.t
diff --git a/kernel/vars.ml b/kernel/vars.ml
index eae917b5a2..b3b3eff628 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -235,49 +235,6 @@ let subst_vars subst c = substn_vars 1 subst c
(** Universe substitutions *)
open Constr
-let subst_univs_fn_puniverses fn =
- let f = Univ.Instance.subst_fn fn in
- fun ((c, u) as x) -> let u' = f u in if u' == u then x else (c, u')
-
-let subst_univs_fn_constr f c =
- let changed = ref false in
- let fu = Univ.subst_univs_universe f in
- let fi = Univ.Instance.subst_fn (Univ.level_subst_of f) in
- let rec aux t =
- match kind t with
- | Sort (Sorts.Type u) ->
- let u' = fu u in
- if u' == u then t else
- (changed := true; mkSort (Sorts.sort_of_univ u'))
- | Const (c, u) ->
- let u' = fi u in
- if u' == u then t
- else (changed := true; mkConstU (c, u'))
- | Ind (i, u) ->
- let u' = fi u in
- if u' == u then t
- else (changed := true; mkIndU (i, u'))
- | Construct (c, u) ->
- let u' = fi u in
- if u' == u then t
- else (changed := true; mkConstructU (c, u'))
- | _ -> map aux t
- in
- let c' = aux c in
- if !changed then c' else c
-
-let subst_univs_constr subst c =
- if Univ.is_empty_subst subst then c
- else
- let f = Univ.make_subst subst in
- subst_univs_fn_constr f c
-
-let subst_univs_constr =
- if Flags.profile then
- let subst_univs_constr_key = CProfile.declare_profile "subst_univs_constr" in
- CProfile.profile2 subst_univs_constr_key subst_univs_constr
- else subst_univs_constr
-
let subst_univs_level_constr subst c =
if Univ.is_empty_level_subst subst then c
else
diff --git a/kernel/vars.mli b/kernel/vars.mli
index 964de4e958..b74d25260f 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -129,12 +129,6 @@ val subst_var : Id.t -> constr -> constr
open Univ
-val subst_univs_fn_constr : universe_subst_fn -> constr -> constr
-val subst_univs_fn_puniverses : universe_level_subst_fn ->
- 'a puniverses -> 'a puniverses
-
-val subst_univs_constr : universe_subst -> constr -> constr
-
(** Level substitutions for polymorphism. *)
val subst_univs_level_constr : universe_level_subst -> constr -> constr
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 19:05:09 +0000