aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cooking.ml190
-rw-r--r--kernel/cooking.mli3
-rw-r--r--kernel/declarations.ml2
-rw-r--r--kernel/indTyping.ml13
-rw-r--r--kernel/indTyping.mli4
-rw-r--r--kernel/inductive.ml8
-rw-r--r--kernel/inductive.mli2
-rw-r--r--kernel/opaqueproof.ml13
-rw-r--r--kernel/opaqueproof.mli2
-rw-r--r--kernel/sorts.ml7
-rw-r--r--kernel/sorts.mli6
-rw-r--r--kernel/term_typing.ml73
-rw-r--r--kernel/type_errors.ml2
-rw-r--r--kernel/type_errors.mli4
14 files changed, 227 insertions, 102 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 13851319cd..620efbafd6 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -165,25 +165,33 @@ type 'opaque result = {
cook_context : Constr.named_context option;
}
-let on_body ml hy f = function
- | Undef _ as x -> x
- | Def cs -> Def (Mod_subst.from_val (f (Mod_subst.force_constr cs)))
- | OpaqueDef o ->
- OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:f
- { Opaqueproof.modlist = ml; abstract = hy } o)
- | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked")
-
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 = (vars, subst, _) } c =
- let cache = RefTable.create 13 in
- let expmod = expmod_constr_subst cache modlist subst in
- let hyps = Context.Named.map expmod vars in
- let hyps = abstract_context hyps in
- abstract_constant_body (expmod c) hyps
+let discharge_abstract_universe_context subst abs_ctx 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, (AUContext.union abs_ctx auctx)
+ else
+ let open Univ in
+ let ainst = make_abstract_instance auctx in
+ let subst = Instance.append subst ainst in
+ let substf = make_instance_subst subst in
+ let auctx = Univ.subst_univs_level_abstract_universe_context substf auctx in
+ subst, (AUContext.union abs_ctx auctx)
let lift_univs cb subst auctx0 =
match cb.const_universes with
@@ -191,26 +199,20 @@ let lift_univs cb subst auctx0 =
assert (AUContext.is_empty auctx0);
subst, (Monomorphic ctx)
| Polymorphic 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 (AUContext.union auctx0 auctx))
- else
- let ainst = Univ.make_abstract_instance auctx in
- let subst = Instance.append subst ainst in
- let substf = Univ.make_instance_subst subst in
- let auctx' = Univ.subst_univs_level_abstract_universe_context substf auctx in
- subst, (Polymorphic (AUContext.union auctx0 auctx'))
+ let subst, auctx = discharge_abstract_universe_context subst auctx0 auctx in
+ subst, (Polymorphic auctx)
+
+let cook_constr { Opaqueproof.modlist ; abstract } c =
+ let cache = RefTable.create 13 in
+ let abstract, usubst, abs_ctx = abstract in
+ (* For now the STM only handles deferred computation of monomorphic
+ constants. The API will need to be adapted when it's not the case
+ anymore. *)
+ let () = assert (AUContext.is_empty abs_ctx) in
+ let expmod = expmod_constr_subst cache modlist usubst in
+ let hyps = Context.Named.map expmod abstract in
+ let hyps = abstract_context hyps in
+ abstract_constant_body (expmod c) hyps
let cook_constant { from = cb; info } =
let { Opaqueproof.modlist; abstract } = info in
@@ -221,9 +223,12 @@ let cook_constant { from = cb; info } =
let hyps0 = Context.Named.map expmod abstract in
let hyps = abstract_context hyps0 in
let map c = abstract_constant_body (expmod c) hyps in
- let body = on_body modlist (hyps0, usubst, abs_ctx)
- map
- cb.const_body
+ let body = match cb.const_body with
+ | Undef _ as x -> x
+ | Def cs -> Def (Mod_subst.from_val (map (Mod_subst.force_constr cs)))
+ | OpaqueDef o ->
+ OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:map info o)
+ | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked")
in
let const_hyps =
Context.Named.fold_outside (fun decl hyps ->
@@ -248,4 +253,115 @@ let cook_constant { from = cb; info } =
(* let cook_constant_key = CProfile.declare_profile "cook_constant" *)
(* let cook_constant = CProfile.profile2 cook_constant_key cook_constant *)
+(********************************)
+(* Discharging mutual inductive *)
+
+(* Replace
+
+ Var(y1)..Var(yq):C1..Cq |- Ij:Bj
+ Var(y1)..Var(yq):C1..Cq; I1..Ip:B1..Bp |- ci : Ti
+
+ by
+
+ |- Ij: (y1..yq:C1..Cq)Bj
+ I1..Ip:(B1 y1..yq)..(Bp y1..yq) |- ci : (y1..yq:C1..Cq)Ti[Ij:=(Ij y1..yq)]
+*)
+
+let it_mkNamedProd_wo_LetIn b d =
+ List.fold_left (fun c d -> mkNamedProd_wo_LetIn d c) b d
+
+let abstract_inductive decls nparamdecls inds =
+ let open Entries in
+ let ntyp = List.length inds in
+ let ndecls = Context.Named.length decls in
+ let args = Context.Named.to_instance mkVar (List.rev decls) in
+ let args = Array.of_list args in
+ let subs = List.init ntyp (fun k -> lift ndecls (mkApp(mkRel (k+1),args))) in
+ let inds' =
+ List.map
+ (function (tname,arity,template,cnames,lc) ->
+ let lc' = List.map (Vars.substl subs) lc in
+ let lc'' = List.map (fun b -> it_mkNamedProd_wo_LetIn b decls) lc' in
+ let arity' = it_mkNamedProd_wo_LetIn arity decls in
+ (tname,arity',template,cnames,lc''))
+ inds in
+ let nparamdecls' = nparamdecls + Array.length args in
+(* To be sure to be the same as before, should probably be moved to cook_inductive *)
+ let params' = let (_,arity,_,_,_) = List.hd inds' in
+ let (params,_) = decompose_prod_n_assum nparamdecls' arity in
+ params
+ in
+ let ind'' =
+ List.map
+ (fun (a,arity,template,c,lc) ->
+ let _, short_arity = decompose_prod_n_assum nparamdecls' arity in
+ let shortlc =
+ List.map (fun c -> snd (decompose_prod_n_assum nparamdecls' c)) lc in
+ { mind_entry_typename = a;
+ mind_entry_arity = short_arity;
+ mind_entry_template = template;
+ mind_entry_consnames = c;
+ mind_entry_lc = shortlc })
+ inds'
+ in (params',ind'')
+
+let refresh_polymorphic_type_of_inductive (_,mip) =
+ match mip.mind_arity with
+ | RegularArity s -> s.mind_user_arity, false
+ | TemplateArity ar ->
+ let ctx = List.rev mip.mind_arity_ctxt in
+ mkArity (List.rev ctx, Sorts.sort_of_univ ar.template_level), true
+
+let dummy_variance = let open Entries in function
+ | Monomorphic_entry _ -> assert false
+ | Polymorphic_entry (_,uctx) -> Array.make (Univ.UContext.size uctx) Univ.Variance.Irrelevant
+
+let cook_inductive { Opaqueproof.modlist; abstract } mib =
+ let open Entries in
+ let (section_decls, subst, abs_uctx) = abstract in
+ let nparamdecls = Context.Rel.length mib.mind_params_ctxt in
+ let subst, ind_univs =
+ match mib.mind_universes with
+ | Monomorphic ctx -> Univ.empty_level_subst, Monomorphic_entry ctx
+ | Polymorphic auctx ->
+ let subst, auctx = discharge_abstract_universe_context subst abs_uctx auctx in
+ let subst = Univ.make_instance_subst subst in
+ let nas = Univ.AUContext.names auctx in
+ let auctx = Univ.AUContext.repr auctx in
+ subst, Polymorphic_entry (nas, auctx)
+ in
+ let variance = match mib.mind_variance with
+ | None -> None
+ | Some _ -> Some (dummy_variance ind_univs)
+ in
+ let cache = RefTable.create 13 in
+ let discharge c = Vars.subst_univs_level_constr subst (expmod_constr cache modlist c) in
+ let inds =
+ Array.map_to_list
+ (fun mip ->
+ let ty, template = refresh_polymorphic_type_of_inductive (mib,mip) in
+ let arity = discharge ty in
+ let lc = Array.map discharge mip.mind_user_lc in
+ (mip.mind_typename,
+ arity, template,
+ Array.to_list mip.mind_consnames,
+ Array.to_list lc))
+ mib.mind_packets in
+ let section_decls' = Context.Named.map discharge section_decls in
+ let (params',inds') = abstract_inductive section_decls' nparamdecls inds in
+ let record = match mib.mind_record with
+ | PrimRecord info ->
+ Some (Some (Array.map (fun (x,_,_,_) -> x) info))
+ | FakeRecord -> Some None
+ | NotRecord -> None
+ in
+ { mind_entry_record = record;
+ mind_entry_finite = mib.mind_finite;
+ mind_entry_params = params';
+ mind_entry_inds = inds';
+ mind_entry_private = mib.mind_private;
+ mind_entry_variance = variance;
+ mind_entry_universes = ind_univs
+ }
+
let expmod_constr modlist c = expmod_constr (RefTable.create 13) modlist c
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 024eed1285..abae3880d7 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -30,6 +30,9 @@ type 'opaque result = {
val cook_constant : recipe -> Opaqueproof.opaque result
val cook_constr : Opaqueproof.cooking_info -> constr -> constr
+val cook_inductive :
+ Opaqueproof.cooking_info -> mutual_inductive_body -> Entries.mutual_inductive_entry
+
(** {6 Utility functions used in module [Discharge]. } *)
val expmod_constr : Opaqueproof.work_list -> constr -> constr
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 860d19fe26..388b4f14bf 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -165,7 +165,7 @@ type one_inductive_body = {
mind_nrealdecls : int; (** Length of realargs context (with let, no params) *)
- mind_kelim : Sorts.family list; (** List of allowed elimination sorts *)
+ mind_kelim : Sorts.family; (** Highest allowed elimination sort *)
mind_nf_lc : (rel_context * types) array; (** Head normalized constructor types so that their conclusion exposes the inductive type *)
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 4e6e595331..65298938fa 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -232,18 +232,9 @@ let check_record data =
(* - all_sorts in case of small, unitary Prop (not smashed) *)
(* - logical_sorts in case of large, unitary Prop (smashed) *)
-let all_sorts = [InSProp;InProp;InSet;InType]
-let small_sorts = [InSProp;InProp;InSet]
-let logical_sorts = [InSProp;InProp]
-let sprop_sorts = [InSProp]
-
let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_;ind_has_relevant_arg=_} =
- if not ind_squashed then all_sorts
- else match Sorts.family (Sorts.sort_of_univ ind_univ) with
- | InType -> assert false
- | InSet -> small_sorts
- | InProp -> logical_sorts
- | InSProp -> sprop_sorts
+ if not ind_squashed then InType
+ else Sorts.family (Sorts.sort_of_univ ind_univ)
(* Returns the list [x_1, ..., x_n] of levels contributing to template
polymorphism. The elements x_k is None if the k-th parameter (starting
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index ad51af66a2..ef2c30b76a 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -22,7 +22,7 @@ open Declarations
- for each inductive,
(arity * constructors) (with params)
* (indices * splayed constructor types) (both without params)
- * allowed eliminations
+ * top allowed elimination
*)
val typecheck_inductive : env -> mutual_inductive_entry ->
env
@@ -31,5 +31,5 @@ val typecheck_inductive : env -> mutual_inductive_entry ->
* Constr.rel_context
* ((inductive_arity * Constr.types array) *
(Constr.rel_context * (Constr.rel_context * Constr.types) array) *
- Sorts.family list)
+ Sorts.family)
array
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index ca7086a3e4..beff8f4421 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -289,7 +289,7 @@ let get_instantiated_arity (_ind,u) (mib,mip) params =
let sign, s = mind_arity mip in
full_inductive_instantiate mib u params sign, s
-let elim_sorts (_,mip) = mip.mind_kelim
+let elim_sort (_,mip) = mip.mind_kelim
let is_private (mib,_) = mib.mind_private = Some true
let is_primitive_record (mib,_) =
@@ -305,12 +305,12 @@ let build_dependent_inductive ind (_,mip) params =
@ Context.Rel.to_extended_list mkRel 0 realargs)
(* This exception is local *)
-exception LocalArity of (Sorts.family list * Sorts.family * Sorts.family * arity_error) option
+exception LocalArity of (Sorts.family * Sorts.family * Sorts.family * arity_error) option
let check_allowed_sort ksort specif =
- if not (CList.exists (Sorts.family_equal ksort) (elim_sorts specif)) then
+ if not (Sorts.family_leq ksort (elim_sort specif)) then
let s = inductive_sort_family (snd specif) in
- raise (LocalArity (Some(elim_sorts specif, ksort,s,error_elim_explain ksort s)))
+ raise (LocalArity (Some(elim_sort specif, ksort,s,error_elim_explain ksort s)))
let is_correct_arity env c pj ind specif params =
let arsign,_ = get_instantiated_arity ind specif params in
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 997a620742..f705cdf646 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -52,7 +52,7 @@ val type_of_inductive : env -> mind_specif puniverses -> types
val type_of_inductive_knowing_parameters :
env -> ?polyprop:bool -> mind_specif puniverses -> types Lazy.t array -> types
-val elim_sorts : mind_specif -> Sorts.family list
+val elim_sort : mind_specif -> Sorts.family
val is_private : mind_specif -> bool
val is_primitive_record : mind_specif -> bool
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 0ff27eb4ea..1971c67c61 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -18,7 +18,6 @@ type work_list = (Instance.t * Id.t array) Cmap.t *
type indirect_accessor = {
access_proof : DirPath.t -> int -> constr option;
- access_constraints : DirPath.t -> int -> Univ.ContextSet.t option;
}
type cooking_info = {
@@ -107,14 +106,12 @@ let force_proof access { opaque_val = prfs; opaque_dir = odp; _ } = function
let c = Future.force pt in
force_constr (List.fold_right subst_substituted l (from_val c))
-let force_constraints access { opaque_val = prfs; opaque_dir = odp; _ } = function
+let force_constraints _access { opaque_val = prfs; opaque_dir = odp; _ } = function
| Direct (_,cu) -> snd(Future.force cu)
| Indirect (_,dp,i) ->
if DirPath.equal dp odp
then snd (Future.force (snd (Int.Map.find i prfs)))
- else match access.access_constraints dp i with
- | None -> Univ.ContextSet.empty
- | Some u -> u
+ else Univ.ContextSet.empty
let get_direct_constraints = function
| Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
@@ -124,15 +121,13 @@ module FMap = Future.UUIDMap
let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ } =
let opaque_table = Array.make n None in
- let univ_table = Array.make n None in
let disch_table = Array.make n [] in
let f2t_map = ref FMap.empty in
let iter n (d, cu) =
let uid = Future.uuid cu in
let () = f2t_map := FMap.add (Future.uuid cu) n !f2t_map in
if Future.is_val cu then
- let (c, u) = Future.force cu in
- let () = univ_table.(n) <- Some u in
+ let (c, _) = Future.force cu in
opaque_table.(n) <- Some c
else if Future.UUIDSet.mem uid except then
disch_table.(n) <- d
@@ -141,4 +136,4 @@ let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _
Pp.(str"Proof object "++int n++str" is not checked nor to be checked")
in
let () = Int.Map.iter iter otab in
- opaque_table, univ_table, disch_table, !f2t_map
+ opaque_table, disch_table, !f2t_map
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 4646206e55..46b0500507 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -37,7 +37,6 @@ val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
type indirect_accessor = {
access_proof : DirPath.t -> int -> constr option;
- access_constraints : DirPath.t -> int -> Univ.ContextSet.t option;
}
(** When stored indirectly, opaque terms are indexed by their library
dirpath and an integer index. The two functions above activate
@@ -70,6 +69,5 @@ val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
val dump : ?except:Future.UUIDSet.t -> opaquetab ->
Constr.t option array *
- Univ.ContextSet.t option array *
cooking_info list array *
int Future.UUIDMap.t
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index 09c98ca1bc..b5a929697e 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -91,6 +91,8 @@ let family_compare a b = match a,b with
let family_equal = (==)
+let family_leq a b = family_compare a b <= 0
+
open Hashset.Combine
let hash = function
@@ -101,11 +103,6 @@ let hash = function
let h = Univ.Universe.hash u in
combinesmall 2 h
-module List = struct
- let mem = List.memq
- let intersect l l' = CList.intersect family_equal l l'
-end
-
module Hsorts =
Hashcons.Make(
struct
diff --git a/kernel/sorts.mli b/kernel/sorts.mli
index c49728b146..3769e31465 100644
--- a/kernel/sorts.mli
+++ b/kernel/sorts.mli
@@ -37,11 +37,7 @@ val hcons : t -> t
val family_compare : family -> family -> int
val family_equal : family -> family -> bool
-
-module List : sig
- val mem : family -> family list -> bool
- val intersect : family list -> family list -> family list
-end
+val family_leq : family -> family -> bool
val univ_of_sort : t -> Univ.Universe.t
val sort_of_univ : Univ.Universe.t -> t
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 088dd98db8..f984088f47 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -115,16 +115,8 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
}
(** Definition [c] is opaque (Qed), non polymorphic and with a specified type,
- so we delay the typing and hash consing of its body.
- Remark: when the universe quantification is given explicitly, we could
- delay even in the polymorphic case. *)
+ so we delay the typing and hash consing of its body. *)
-(** Definition is opaque (Qed) and non polymorphic with known type, so we delay
-the typing and hash consing of its body.
-
-TODO: if the universe quantification is given explicitly, we could delay even in
-the polymorphic case
- *)
| DefinitionEntry ({ const_entry_type = Some typ;
const_entry_opaque = true;
const_entry_universes = Monomorphic_entry univs; _ } as c) ->
@@ -165,16 +157,59 @@ the polymorphic case
cook_context = c.const_entry_secctx;
}
+ (** Similar case for polymorphic entries. TODO: also delay type-checking of
+ the body. *)
+
+ | DefinitionEntry ({ const_entry_type = Some typ;
+ const_entry_opaque = true;
+ const_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) ->
+ let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in
+ let env = push_context ~strict:false uctx env in
+ let tj = Typeops.infer_type env typ in
+ let sbst, auctx = Univ.abstract_universes nas uctx in
+ let usubst = Univ.make_instance_subst sbst in
+ let (def, private_univs) =
+ let (body, ctx), side_eff = Future.join body in
+ let body, ctx = match trust with
+ | Pure -> body, ctx
+ | SideEffects handle ->
+ let body, ctx', _ = handle env body side_eff in
+ body, Univ.ContextSet.union ctx ctx'
+ in
+ (** [ctx] must contain local universes, such that it has no impact
+ on the rest of the graph (up to transitivity). *)
+ let env = push_subgraph ctx env in
+ let private_univs = on_snd (Univ.subst_univs_level_constraints usubst) ctx in
+ let j = Typeops.infer env body in
+ let _ = Typeops.judge_of_cast env j DEFAULTcast tj in
+ let def = Vars.subst_univs_level_constr usubst j.uj_val in
+ def, private_univs
+ in
+ let def = OpaqueDef (Future.from_val (def, Univ.ContextSet.empty)) in
+ let typ = Vars.subst_univs_level_constr usubst tj.utj_val in
+ feedback_completion_typecheck feedback_id;
+ {
+ Cooking.cook_body = def;
+ cook_type = typ;
+ cook_universes = Polymorphic auctx;
+ cook_private_univs = Some private_univs;
+ cook_relevance = Sorts.relevance_of_sort tj.utj_type;
+ cook_inline = c.const_entry_inline_code;
+ cook_context = c.const_entry_secctx;
+ }
+
(** Other definitions have to be processed immediately. *)
| DefinitionEntry c ->
- let { const_entry_type = typ; const_entry_opaque = opaque ; _ } = c in
+ let { const_entry_type = typ; _ } = c in
let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in
- let (body, ctx), side_eff = Future.join body in
+ (* Opaque constants must be provided with a non-empty const_entry_type,
+ and thus should have been treated above. *)
+ let () = assert (not c.const_entry_opaque) in
let body, ctx = match trust with
- | Pure -> body, ctx
- | SideEffects handle ->
- let body, ctx', _ = handle env body side_eff in
- body, Univ.ContextSet.union ctx ctx'
+ | Pure ->
+ let (body, ctx), () = Future.join body in
+ body, ctx
+ | SideEffects _ -> assert false
in
let env, usubst, univs, private_univs = match c.const_entry_universes with
| Monomorphic_entry univs ->
@@ -188,9 +223,6 @@ the polymorphic case
let sbst, auctx = Univ.abstract_universes nas uctx in
let sbst = Univ.make_instance_subst sbst in
let env, local =
- if opaque then
- push_subgraph ctx env, Some (on_snd (Univ.subst_univs_level_constraints sbst) ctx)
- else
if Univ.ContextSet.is_empty ctx then env, None
else CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.")
in
@@ -206,10 +238,7 @@ the polymorphic case
Vars.subst_univs_level_constr usubst tj.utj_val
in
let def = Vars.subst_univs_level_constr usubst j.uj_val in
- let def =
- if opaque then OpaqueDef (Future.from_val (def, Univ.ContextSet.empty))
- else Def (Mod_subst.from_val def)
- in
+ let def = Def (Mod_subst.from_val def) in
feedback_completion_typecheck feedback_id;
{
Cooking.cook_body = def;
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index c45fe1cf00..857e4fabf7 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -49,7 +49,7 @@ type ('constr, 'types) ptype_error =
| BadAssumption of ('constr, 'types) punsafe_judgment
| ReferenceVariables of Id.t * 'constr
| ElimArity of pinductive * 'constr * ('constr, 'types) punsafe_judgment
- * (Sorts.family list * Sorts.family * Sorts.family * arity_error) option
+ * (Sorts.family * Sorts.family * Sorts.family * arity_error) option
| CaseNotInductive of ('constr, 'types) punsafe_judgment
| WrongCaseInfo of pinductive * case_info
| NumberBranches of ('constr, 'types) punsafe_judgment * int
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 88165a4f07..8e25236851 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -50,7 +50,7 @@ type ('constr, 'types) ptype_error =
| BadAssumption of ('constr, 'types) punsafe_judgment
| ReferenceVariables of Id.t * 'constr
| ElimArity of pinductive * 'constr * ('constr, 'types) punsafe_judgment
- * (Sorts.family list * Sorts.family * Sorts.family * arity_error) option
+ * (Sorts.family * Sorts.family * Sorts.family * arity_error) option
| CaseNotInductive of ('constr, 'types) punsafe_judgment
| WrongCaseInfo of pinductive * case_info
| NumberBranches of ('constr, 'types) punsafe_judgment * int
@@ -104,7 +104,7 @@ val error_reference_variables : env -> Id.t -> constr -> 'a
val error_elim_arity :
env -> pinductive -> constr -> unsafe_judgment ->
- (Sorts.family list * Sorts.family * Sorts.family * arity_error) option -> 'a
+ (Sorts.family * Sorts.family * Sorts.family * arity_error) option -> 'a
val error_case_not_inductive : env -> unsafe_judgment -> 'a
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 01:58:12 +0000