aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/classes.ml10
-rw-r--r--vernac/command.ml47
-rw-r--r--vernac/command.mli10
-rw-r--r--vernac/discharge.ml24
-rw-r--r--vernac/discharge.mli3
-rw-r--r--vernac/himsg.ml4
-rw-r--r--vernac/ind_tables.ml4
-rw-r--r--vernac/obligations.ml4
-rw-r--r--vernac/record.ml70
-rw-r--r--vernac/record.mli6
-rw-r--r--vernac/search.ml2
-rw-r--r--vernac/vernacentries.ml22
12 files changed, 141 insertions, 65 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index aba61146c7..007b70bc0f 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -114,8 +114,8 @@ let instance_hook k info global imps ?hook cst =
let declare_instance_constant k info global imps ?hook id pl poly evm term termtype =
let kind = IsDefinition Instance in
let evm =
- let levels = Univ.LSet.union (Universes.universes_of_constr termtype)
- (Universes.universes_of_constr term) in
+ let levels = Univ.LSet.union (Univops.universes_of_constr termtype)
+ (Univops.universes_of_constr term) in
Evd.restrict_universe_context evm levels
in
let pl, uctx = Evd.universe_context ?names:pl evm in
@@ -420,6 +420,8 @@ let context poly l =
let _ = Command.declare_definition id decl entry [] [] hook in
Lib.sections_are_opened () || Lib.is_modtype_strict ()
in
- let () = uctx := Univ.ContextSet.empty in
status && nstatus
- in List.fold_left fn true (List.rev ctx)
+ in
+ if Lib.sections_are_opened () then
+ Declare.declare_universe_context poly !uctx;
+ List.fold_left fn true (List.rev ctx)
diff --git a/vernac/command.ml b/vernac/command.ml
index 998e7803e1..4064773561 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -106,7 +106,7 @@ let interp_definition pl bl p red_option c ctypopt =
let c = EConstr.Unsafe.to_constr c in
let nf,subst = Evarutil.e_nf_evars_and_universes evdref in
let body = nf (it_mkLambda_or_LetIn c ctx) in
- let vars = Universes.universes_of_constr body in
+ let vars = Univops.universes_of_constr body in
let evd = Evd.restrict_universe_context !evdref vars in
let pl, uctx = Evd.universe_context ?names:pl evd in
imps1@(Impargs.lift_implicits nb_args imps2), pl,
@@ -131,8 +131,8 @@ let interp_definition pl bl p red_option c ctypopt =
in
if not (try List.for_all chk imps2 with Not_found -> false)
then warn_implicits_in_term ();
- let vars = Univ.LSet.union (Universes.universes_of_constr body)
- (Universes.universes_of_constr typ) in
+ let vars = Univ.LSet.union (Univops.universes_of_constr body)
+ (Univops.universes_of_constr typ) in
let ctx = Evd.restrict_universe_context !evdref vars in
let pl, uctx = Evd.universe_context ?names:pl ctx in
imps1@(Impargs.lift_implicits nb_args impsty), pl,
@@ -329,7 +329,7 @@ let do_assumptions_bound_univs coe kind nl id pl c =
let nf, subst = Evarutil.e_nf_evars_and_universes evdref in
let ty = EConstr.Unsafe.to_constr ty in
let ty = nf ty in
- let vars = Universes.universes_of_constr ty in
+ let vars = Univops.universes_of_constr ty in
let evd = Evd.restrict_universe_context !evdref vars in
let pl, uctx = Evd.universe_context ?names:pl evd in
let uctx = Univ.ContextSet.of_context uctx in
@@ -573,7 +573,7 @@ let check_param = function
| CLocalAssum (nas, Generalized _, _) -> ()
| CLocalPattern _ -> assert false
-let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
+let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
check_all_names_different indl;
List.iter check_param paramsl;
let env0 = Global.env() in
@@ -649,16 +649,27 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
indimpls, List.map (fun impls ->
userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors
in
+ let univs =
+ if poly then
+ if cum then
+ Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context uctx)
+ else Polymorphic_ind_entry uctx
+ else
+ Monomorphic_ind_entry uctx
+ in
(* Build the mutual inductive entry *)
- { mind_entry_params = List.map prepare_param ctx_params;
- mind_entry_record = None;
- mind_entry_finite = finite;
- mind_entry_inds = entries;
- mind_entry_polymorphic = poly;
- mind_entry_private = if prv then Some false else None;
- mind_entry_universes = uctx;
- },
- pl, impls
+ let mind_ent =
+ { mind_entry_params = List.map prepare_param ctx_params;
+ mind_entry_record = None;
+ mind_entry_finite = finite;
+ mind_entry_inds = entries;
+ mind_entry_private = if prv then Some false else None;
+ mind_entry_universes = univs;
+ }
+ in
+ (if poly && cum then
+ Inductiveops.infer_inductive_subtyping env_ar evd mind_ent
+ else mind_ent), pl, impls
(* Very syntactical equality *)
let eq_local_binders bl1 bl2 =
@@ -742,10 +753,10 @@ type one_inductive_impls =
Impargs.manual_explicitation list (* for inds *)*
Impargs.manual_explicitation list list (* for constrs *)
-let do_mutual_inductive indl poly prv finite =
+let do_mutual_inductive indl cum poly prv finite =
let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in
(* Interpret the types *)
- let mie,pl,impls = interp_mutual_inductive indl ntns poly prv finite in
+ let mie,pl,impls = interp_mutual_inductive indl ntns cum poly prv finite in
(* Declare the mutual inductive block with its associated schemes *)
ignore (declare_mutual_inductive_with_eliminations mie pl impls);
(* Declare the possible notations of inductive types *)
@@ -1208,7 +1219,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
let env = Global.env() in
let indexes = search_guard env indexes fixdecls in
let fiximps = List.map (fun (n,r,p) -> r) fiximps in
- let vars = Universes.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
+ let vars = Univops.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
let fixdecls =
List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
let evd = Evd.from_ctx ctx in
@@ -1240,7 +1251,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
let fixdefs = List.map Option.get fixdefs in
let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
- let vars = Universes.universes_of_constr (List.hd fixdecls) in
+ let vars = Univops.universes_of_constr (List.hd fixdecls) in
let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
let evd = Evd.from_ctx ctx in
diff --git a/vernac/command.mli b/vernac/command.mli
index 2a52d9bcb5..a636bc03c5 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -90,9 +90,9 @@ type one_inductive_impls =
Impargs.manual_implicits list (** for constrs *)
val interp_mutual_inductive :
- structured_inductive_expr -> decl_notation list -> polymorphic ->
- private_flag -> Decl_kinds.recursivity_kind ->
- mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list
+ structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag ->
+ polymorphic -> private_flag -> Decl_kinds.recursivity_kind ->
+ mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list
(** Registering a mutual inductive definition together with its
associated schemes *)
@@ -104,8 +104,8 @@ val declare_mutual_inductive_with_eliminations :
(** Entry points for the vernacular commands Inductive and CoInductive *)
val do_mutual_inductive :
- (one_inductive_expr * decl_notation list) list -> polymorphic ->
- private_flag -> Decl_kinds.recursivity_kind -> unit
+ (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag ->
+ polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> unit
(** {6 Fixpoints and cofixpoints} *)
diff --git a/vernac/discharge.ml b/vernac/discharge.ml
index 65ade78876..18f93334b1 100644
--- a/vernac/discharge.ml
+++ b/vernac/discharge.ml
@@ -79,12 +79,14 @@ let refresh_polymorphic_type_of_inductive (_,mip) =
let process_inductive (sechyps,abs_ctx) modlist mib =
let nparams = mib.mind_nparams in
- let subst, univs =
- if mib.mind_polymorphic then
- let inst = Univ.UContext.instance mib.mind_universes in
- let cstrs = Univ.UContext.constraints mib.mind_universes in
- inst, Univ.UContext.make (inst, Univ.subst_instance_constraints inst cstrs)
- else Univ.Instance.empty, mib.mind_universes
+ let subst, univs =
+ match mib.mind_universes with
+ | Monomorphic_ind ctx -> Univ.Instance.empty, ctx
+ | Polymorphic_ind auctx ->
+ Univ.AUContext.instance auctx, Univ.instantiate_univ_context auctx
+ | Cumulative_ind cumi ->
+ let auctx = Univ.ACumulativityInfo.univ_context cumi in
+ Univ.AUContext.instance auctx, Univ.instantiate_univ_context auctx
in
let inds =
Array.map_to_list
@@ -105,6 +107,12 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
let (params',inds') = abstract_inductive sechyps' nparams inds in
let abs_ctx = Univ.instantiate_univ_context abs_ctx in
let univs = Univ.UContext.union abs_ctx univs in
+ let ind_univs =
+ match mib.mind_universes with
+ | Monomorphic_ind _ -> Monomorphic_ind_entry univs
+ | Polymorphic_ind _ -> Polymorphic_ind_entry univs
+ | Cumulative_ind _ ->
+ Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs) in
let record = match mib.mind_record with
| Some (Some (id, _, _)) -> Some (Some id)
| Some None -> Some None
@@ -114,7 +122,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
mind_entry_finite = mib.mind_finite;
mind_entry_params = params';
mind_entry_inds = inds';
- mind_entry_polymorphic = mib.mind_polymorphic;
mind_entry_private = mib.mind_private;
- mind_entry_universes = univs;
+ mind_entry_universes = ind_univs
}
+
diff --git a/vernac/discharge.mli b/vernac/discharge.mli
index 18d1b67766..3845c04a11 100644
--- a/vernac/discharge.mli
+++ b/vernac/discharge.mli
@@ -11,4 +11,5 @@ open Entries
open Opaqueproof
val process_inductive :
- Context.Named.t Univ.in_universe_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry
+ ((Term.constr, Term.constr) Context.Named.pt * Univ.abstract_universe_context)
+ -> work_list -> mutual_inductive_body -> mutual_inductive_entry
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 6d8dd82ac6..ce91e1a09f 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -889,6 +889,10 @@ let explain_not_match_error = function
| NoTypeConstraintExpected ->
strbrk "a definition whose type is constrained can only be subtype " ++
strbrk "of a definition whose type is itself constrained"
+ | CumulativeStatusExpected b ->
+ let status b = if b then str"cumulative" else str"non-cumulative" in
+ str "a " ++ status b ++ str" declaration was expected, but a " ++
+ status (not b) ++ str" declaration was found"
| PolymorphicStatusExpected b ->
let status b = if b then str"polymorphic" else str"monomorphic" in
str "a " ++ status b ++ str" declaration was expected, but a " ++
diff --git a/vernac/ind_tables.ml b/vernac/ind_tables.ml
index f3259f1f3b..65d42b6267 100644
--- a/vernac/ind_tables.ml
+++ b/vernac/ind_tables.ml
@@ -148,7 +148,7 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
let id = match idopt with
| Some id -> id
| None -> add_suffix mib.mind_packets.(i).mind_typename suff in
- let const = define mode id c mib.mind_polymorphic ctx in
+ let const = define mode id c (Declareops.inductive_is_polymorphic mib) ctx in
declare_scheme kind [|ind,const|];
const, Safe_typing.add_private
(Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind,const]) eff
@@ -166,7 +166,7 @@ let define_mutual_scheme_base kind suff f mode names mind =
try Int.List.assoc i names
with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in
let consts = Array.map2 (fun id cl ->
- define mode id cl mib.mind_polymorphic ctx) ids cl in
+ define mode id cl (Declareops.inductive_is_polymorphic mib) ctx) ids cl in
let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in
declare_scheme kind schemes;
consts,
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index e03e9b8039..135e4c63ab 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -365,8 +365,8 @@ let get_body obl =
match obl.obl_body with
| None -> None
| Some (DefinedObl c) ->
- let ctx = Environ.constant_context (Global.env ()) c in
- let pc = (c, Univ.UContext.instance ctx) in
+ let u = Environ.constant_instance (Global.env ()) c in
+ let pc = (c, u) in
Some (DefinedObl pc)
| Some (TermObl c) ->
Some (TermObl c)
diff --git a/vernac/record.ml b/vernac/record.ml
index 2400fa6814..7dd70d0133 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -265,10 +265,16 @@ let warn_non_primitive_record =
let declare_projections indsp ?(kind=StructureComponent) binder_name coers fieldimpls fields =
let env = Global.env() in
let (mib,mip) = Global.lookup_inductive indsp in
- let u = Declareops.inductive_instance mib in
+ let u = Declareops.inductive_polymorphic_instance mib in
let paramdecls = Inductive.inductive_paramdecls (mib, u) in
- let poly = mib.mind_polymorphic in
- let ctx = Univ.instantiate_univ_context mib.mind_universes in
+ let poly = Declareops.inductive_is_polymorphic mib in
+ let ctx =
+ match mib.mind_universes with
+ | Monomorphic_ind ctx -> ctx
+ | Polymorphic_ind auctx -> Univ.instantiate_univ_context auctx
+ | Cumulative_ind cumi ->
+ Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi)
+ in
let indu = indsp, u in
let r = mkIndU (indsp,u) in
let rp = applist (r, Context.Rel.to_extended_list mkRel 0 paramdecls) in
@@ -377,12 +383,18 @@ let structure_signature ctx =
open Typeclasses
-let declare_structure finite poly ctx id idbuild paramimpls params arity template
+let declare_structure finite univs id idbuild paramimpls params arity template
fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign =
let nparams = List.length params and nfields = List.length fields in
let args = Context.Rel.to_extended_list mkRel nfields params in
let ind = applist (mkRel (1+nparams+nfields), args) in
let type_constructor = it_mkProd_or_LetIn ind fields in
+ let poly, ctx =
+ match univs with
+ | Monomorphic_ind_entry ctx -> false, ctx
+ | Polymorphic_ind_entry ctx -> true, ctx
+ | Cumulative_ind_entry cumi -> true, (Univ.CumulativityInfo.univ_context cumi)
+ in
let binder_name =
match name with
| None -> Id.of_string (Unicode.lowercase_first_char (Id.to_string id))
@@ -400,11 +412,22 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity templat
mind_entry_record = Some (if !primitive_flag then Some binder_name else None);
mind_entry_finite = finite;
mind_entry_inds = [mie_ind];
- mind_entry_polymorphic = poly;
mind_entry_private = None;
- mind_entry_universes = ctx;
+ mind_entry_universes = univs;
}
in
+ let mie =
+ if poly then
+ begin
+ let env = Global.env () in
+ let env' = Environ.push_context ctx env in
+ (* let env'' = Environ.push_rel_context params env' in *)
+ let evd = Evd.from_env env' in
+ Inductiveops.infer_inductive_subtyping env' evd mie
+ end
+ else
+ mie
+ in
let kn = Command.declare_mutual_inductive_with_eliminations mie [] [(paramimpls,[])] in
let rsp = (kn,0) in (* This is ind path of idstruc *)
let cstr = (rsp,1) in
@@ -423,7 +446,7 @@ let implicits_of_context ctx =
in ExplByPos (i, explname), (true, true, true))
1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
-let declare_class finite def poly ctx id idbuild paramimpls params arity
+let declare_class finite def cum poly ctx id idbuild paramimpls params arity
template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign =
let fieldimpls =
(* Make the class implicit in the projections, and the params if applicable. *)
@@ -466,7 +489,16 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity
in
cref, [Name proj_name, sub, Some proj_cst]
| _ ->
- let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls
+ let univs =
+ if poly then
+ if cum then
+ Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context ctx)
+ else
+ Polymorphic_ind_entry ctx
+ else
+ Monomorphic_ind_entry ctx
+ in
+ let ind = declare_structure BiFinite univs (snd id) idbuild paramimpls
params arity template fieldimpls fields
~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign
in
@@ -515,7 +547,7 @@ let add_inductive_class ind =
let mind, oneind = Global.lookup_inductive ind in
let k =
let ctx = oneind.mind_arity_ctxt in
- let inst = Univ.UContext.instance mind.mind_universes in
+ let inst = Declareops.inductive_polymorphic_instance mind in
let ty = Inductive.type_of_inductive
(push_rel_context ctx (Global.env ()))
((mind,oneind),inst)
@@ -540,7 +572,7 @@ open Vernacexpr
(* [fs] corresponds to fields and [ps] to parameters; [coers] is a
list telling if the corresponding fields must me declared as coercions
or subinstances. *)
-let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,idbuild,s) =
+let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,idbuild,s) =
let cfs,notations = List.split cfs in
let cfs,priorities = List.split cfs in
let coers,fs = List.split cfs in
@@ -564,14 +596,24 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id
let gr = match kind with
| Class def ->
let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in
- let gr = declare_class finite def poly ctx (loc,idstruc) idbuild
+ let gr = declare_class finite def cum poly ctx (loc,idstruc) idbuild
implpars params arity template implfs fields is_coe coers priorities sign in
gr
| _ ->
- let implfs = List.map
+ let implfs = List.map
(fun impls -> implpars @ Impargs.lift_implicits
- (succ (List.length params)) impls) implfs in
- let ind = declare_structure finite poly ctx idstruc
+ (succ (List.length params)) impls) implfs
+ in
+ let univs =
+ if poly then
+ if cum then
+ Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context ctx)
+ else
+ Polymorphic_ind_entry ctx
+ else
+ Monomorphic_ind_entry ctx
+ in
+ let ind = declare_structure finite univs idstruc
idbuild implpars params arity template implfs
fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in
IndRef ind
diff --git a/vernac/record.mli b/vernac/record.mli
index 3fd651db90..aa530fd61a 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -26,7 +26,7 @@ val declare_projections :
val declare_structure :
Decl_kinds.recursivity_kind ->
- bool (** polymorphic?*) -> Univ.universe_context ->
+ Entries.inductive_universes ->
Id.t -> Id.t ->
manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *)
bool (** template arity ? *) ->
@@ -38,8 +38,8 @@ val declare_structure :
inductive
val definition_structure :
- inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind *
- plident with_coercion * local_binder_expr list *
+ inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic *
+ Decl_kinds.recursivity_kind * plident with_coercion * local_binder_expr list *
(local_decl_expr with_instance with_priority with_notation) list *
Id.t * constr_expr option -> global_reference
diff --git a/vernac/search.ml b/vernac/search.ml
index 0ff78f439d..5e56ada8ad 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -85,7 +85,7 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) =
let mib = Global.lookup_mind mind in
let iter_packet i mip =
let ind = (mind, i) in
- let u = Declareops.inductive_instance mib in
+ let u = Declareops.inductive_polymorphic_instance mib in
let i = (ind, u) in
let typ = Inductiveops.type_of_inductive env i in
let () = fn (IndRef ind) env typ in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index d0f9c7de74..21f053fb9b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -526,7 +526,7 @@ let vernac_assumption locality poly (local, kind) l nl =
let status = do_assumptions kind nl l in
if not status then Feedback.feedback Feedback.AddedAxiom
-let vernac_record k poly finite struc binders sort nameopt cfs =
+let vernac_record cum k poly finite struc binders sort nameopt cfs =
let const = match nameopt with
| None -> add_prefix "Build_" (snd (fst (snd struc)))
| Some (_,id as lid) ->
@@ -537,13 +537,13 @@ let vernac_record k poly finite struc binders sort nameopt cfs =
match x with
| Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj"
| _ -> ()) cfs);
- ignore(Record.definition_structure (k,poly,finite,struc,binders,cfs,const,sort))
+ ignore(Record.definition_structure (k,cum,poly,finite,struc,binders,cfs,const,sort))
(** When [poly] is true the type is declared polymorphic. When [lo] is true,
then the type is declared private (as per the [Private] keyword). [finite]
indicates whether the type is inductive, co-inductive or
neither. *)
-let vernac_inductive poly lo finite indl =
+let vernac_inductive cum poly lo finite indl =
if Dumpglob.dump () then
List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) ->
match cstrs with
@@ -559,14 +559,14 @@ let vernac_inductive poly lo finite indl =
| [ (_ , _ , _ ,Variant, RecordDecl _),_ ] ->
user_err Pp.(str "The Variant keyword does not support syntax { ... }.")
| [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] ->
- vernac_record (match b with Class _ -> Class false | _ -> b)
+ vernac_record cum (match b with Class _ -> Class false | _ -> b)
poly finite id bl c oc fs
| [ ( id , bl , c , Class _, Constructors [l]), [] ] ->
let f =
let (coe, ((loc, id), ce)) = l in
let coe' = if coe then Some true else None in
(((coe', AssumExpr ((loc, Name id), ce)), None), [])
- in vernac_record (Class true) poly finite id bl c None [f]
+ in vernac_record cum (Class true) poly finite id bl c None [f]
| [ ( _ , _, _, Class _, Constructors _), [] ] ->
user_err Pp.(str "Inductive classes not supported")
| [ ( id , bl , c , Class _, _), _ :: _ ] ->
@@ -580,7 +580,7 @@ let vernac_inductive poly lo finite indl =
| _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.")
in
let indl = List.map unpack indl in
- do_mutual_inductive indl poly lo finite
+ do_mutual_inductive indl cum poly lo finite
let vernac_fixpoint locality poly local l =
let local = enforce_locality_exp locality local in
@@ -1365,6 +1365,14 @@ let _ =
optwrite = Flags.make_universe_polymorphism }
let _ =
+ declare_bool_option
+ { optdepr = false;
+ optname = "inductive cumulativity";
+ optkey = ["Inductive"; "Cumulativity"];
+ optread = Flags.is_inductive_cumulativity;
+ optwrite = Flags.make_inductive_cumulativity }
+
+let _ =
declare_int_option
{ optdepr = false;
optname = "the level of inlining during functor application";
@@ -1933,7 +1941,7 @@ let interp ?proof ?loc locality poly c =
| VernacEndProof e -> vernac_end_proof ?proof e
| VernacExactProof c -> vernac_exact_proof c
| VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl
- | VernacInductive (priv,finite,l) -> vernac_inductive poly priv finite l
+ | VernacInductive (cum, priv,finite,l) -> vernac_inductive cum poly priv finite l
| VernacFixpoint (local, l) -> vernac_fixpoint locality poly local l
| VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l
| VernacScheme l -> vernac_scheme l
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 08:12:56 +0000