aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--intf/decl_kinds.mli2
-rw-r--r--intf/vernacexpr.mli2
-rw-r--r--kernel/declarations.mli4
-rw-r--r--kernel/declareops.ml3
-rw-r--r--kernel/entries.mli3
-rw-r--r--kernel/indtypes.ml6
-rw-r--r--kernel/modops.ml5
-rw-r--r--library/declare.ml3
-rw-r--r--parsing/g_vernac.ml412
-rw-r--r--plugins/funind/glob_term_to_relation.ml6
-rw-r--r--plugins/funind/merge.ml3
-rw-r--r--pretyping/cases.ml1
-rw-r--r--pretyping/indrec.ml22
-rw-r--r--pretyping/tacred.ml8
-rw-r--r--pretyping/tacred.mli5
-rw-r--r--printing/ppvernac.ml2
-rw-r--r--stm/vernac_classifier.ml2
-rw-r--r--tactics/equality.ml6
-rw-r--r--toplevel/command.ml9
-rw-r--r--toplevel/command.mli6
-rw-r--r--toplevel/discharge.ml1
-rw-r--r--toplevel/record.ml1
-rw-r--r--toplevel/vernacentries.ml6
23 files changed, 82 insertions, 36 deletions
diff --git a/intf/decl_kinds.mli b/intf/decl_kinds.mli
index 2ed776c2d..ff77d718b 100644
--- a/intf/decl_kinds.mli
+++ b/intf/decl_kinds.mli
@@ -14,6 +14,8 @@ type binding_kind = Explicit | Implicit
type polymorphic = bool
+type private_flag = bool
+
type theorem_kind =
| Theorem
| Lemma
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index ed6ded8e1..0b2e55941 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -296,7 +296,7 @@ type vernac_expr =
| VernacExactProof of constr_expr
| VernacAssumption of (locality option * assumption_object_kind) *
inline * simple_binder with_coercion list
- | VernacInductive of inductive_flag * infer_flag * (inductive_expr * decl_notation list) list
+ | VernacInductive of private_flag * inductive_flag * infer_flag * (inductive_expr * decl_notation list) list
| VernacFixpoint of
locality option * (fixpoint_expr * decl_notation list) list
| VernacCoFixpoint of
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index f269e165e..9c7344f89 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -172,7 +172,9 @@ type mutual_inductive_body = {
mind_universes : Univ.universe_context; (** Local universe variables and constraints *)
- }
+ mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
+
+}
(** {6 Module declarations } *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 92a566b7c..8806bba45 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -227,7 +227,8 @@ let subst_mind_body sub mib =
Context.map_rel_context (subst_mps sub) mib.mind_params_ctxt;
mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ;
mind_polymorphic = mib.mind_polymorphic;
- mind_universes = mib.mind_universes }
+ mind_universes = mib.mind_universes;
+ mind_private = mib.mind_private }
(** {6 Hash-consing of inductive declarations } *)
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 1bc3bbd15..a161a6fcb 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -46,7 +46,8 @@ type mutual_inductive_entry = {
mind_entry_params : (Id.t * local_entry) list;
mind_entry_inds : one_inductive_entry list;
mind_entry_polymorphic : bool;
- mind_entry_universes : Univ.universe_context }
+ mind_entry_universes : Univ.universe_context;
+ mind_entry_private : bool option }
(** {6 Constants (Definition/Axiom) } *)
type proof_output = constr * Declareops.side_effects
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index e89bbf0d9..73fdaa81f 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -628,6 +628,7 @@ let used_section_variables env inds =
(fun l c -> Id.Set.union (Environ.global_vars_set env c) l)
Id.Set.empty inds in
keep_hyps env ids
+
let lift_decl n d =
map_rel_declaration (lift n) d
@@ -660,7 +661,7 @@ let compute_expansion ((kn, _ as ind), u) params ctx =
(Array.map (fun p -> mkProj (p, mkRel 1)) projarr))
in exp, projarr
-let build_inductive env p ctx env_ar params kn isrecord isfinite inds nmr recargs =
+let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr recargs =
let ntypes = Array.length inds in
(* Compute the set of used section variables *)
let hyps = used_section_variables env inds in
@@ -743,6 +744,7 @@ let build_inductive env p ctx env_ar params kn isrecord isfinite inds nmr recarg
mind_packets = packets;
mind_polymorphic = p;
mind_universes = ctx;
+ mind_private = prv;
}
(************************************************************************)
@@ -757,7 +759,7 @@ let check_inductive env kn mie =
(* Then check positivity conditions *)
let (nmr,recargs) = check_positivity kn env_ar params inds in
(* Build the inductive packets *)
- build_inductive env mie.mind_entry_polymorphic
+ build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private
mie.mind_entry_universes
env_ar params kn mie.mind_entry_record mie.mind_entry_finite
inds nmr recargs
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 093ee7024..4c18ed275 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -308,6 +308,11 @@ let rec add_structure mp sign resolver linkinfo env =
Environ.add_constant_key c cb linkinfo env
|SFBmind mib ->
let mind = mind_of_delta_kn resolver (KerName.make2 mp l) in
+ let mib =
+ if mib.mind_private != None then
+ { mib with mind_private = Some true }
+ else mib
+ in
Environ.add_mind_key mind (mib,linkinfo) env
|SFBmodule mb -> add_module mb linkinfo env (* adds components as well *)
|SFBmodtype mtb -> Environ.add_modtype mtb env
diff --git a/library/declare.ml b/library/declare.ml
index 45015ac65..7fbf2f5ac 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -358,7 +358,8 @@ let dummy_inductive_entry (_,m) = ([],{
mind_entry_finite = true;
mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds;
mind_entry_polymorphic = false;
- mind_entry_universes = Univ.UContext.empty })
+ mind_entry_universes = Univ.UContext.empty;
+ mind_entry_private = None })
type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index df3c18d10..05e654925 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -190,11 +190,11 @@ GEXTEND Gram
| IDENT "Let"; id = identref; b = def_body ->
VernacDefinition ((Some Discharge, Definition), id, b)
(* Gallina inductive declarations *)
- | f = finite_token;
+ | priv = private_token; f = finite_token;
indl = LIST1 inductive_definition SEP "with" ->
let (k,f) = f in
let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
- VernacInductive (f,false,indl)
+ VernacInductive (priv,f,false,indl)
| "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
VernacFixpoint (None, recs)
| IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
@@ -212,13 +212,14 @@ GEXTEND Gram
;
gallina_ext:
- [ [ b = record_token; infer = infer_token; oc = opt_coercion; name = identref;
+ [ [ priv = private_token;
+ b = record_token; infer = infer_token; oc = opt_coercion; name = identref;
ps = binders;
s = OPT [ ":"; s = lconstr -> s ];
cfs = [ ":="; l = constructor_list_or_record_decl -> l
| -> RecordDecl (None, []) ] ->
let (recf,indf) = b in
- VernacInductive (indf,infer,[((oc,name),ps,s,recf,cfs),[]])
+ VernacInductive (priv,indf,infer,[((oc,name),ps,s,recf,cfs),[]])
] ]
;
thm_token:
@@ -260,6 +261,9 @@ GEXTEND Gram
infer_token:
[ [ IDENT "Infer" -> true | -> false ] ]
;
+ private_token:
+ [ [ IDENT "Private" -> true | -> false ] ]
+ ;
record_token:
[ [ IDENT "Record" -> (Record,BiFinite)
| IDENT "Structure" -> (Structure,BiFinite)
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 4544f736c..41970fce8 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1405,7 +1405,7 @@ let do_build_inductive
(* in *)
let _time2 = System.get_time () in
try
- with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds false)) true
+ with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds false false)) true
with
| UserError(s,msg) as e ->
let _time3 = System.get_time () in
@@ -1416,7 +1416,7 @@ let do_build_inductive
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds))
+ Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,false,repacked_rel_inds))
++ fnl () ++
msg
in
@@ -1431,7 +1431,7 @@ let do_build_inductive
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds))
+ Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,false,repacked_rel_inds))
++ fnl () ++
Errors.print reraise
in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 2e524a35f..6eabe6e87 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -884,7 +884,8 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
(* Declare inductive *)
let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in
- let mie,impls = Command.interp_mutual_inductive indl [] false (*FIXMEnon-poly *) true (* means: not coinductive *) in
+ let mie,impls = Command.interp_mutual_inductive indl []
+ false (*FIXMEnon-poly *) false (* means not private *) true (* means: not coinductive *) in
(* Declare the mutual inductive block with its associated schemes *)
ignore (Command.declare_mutual_inductive_with_eliminations Declare.UserVerbose mie impls)
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index b56d5947c..2b0a2dda9 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1298,6 +1298,7 @@ and match_current pb (initial,tomatch) =
compile_all_variables initial tomatch pb
| IsInd (_,(IndType(indf,realargs) as indt),names) ->
let mind,_ = dest_ind_family indf in
+ let mind = Tacred.check_privacy pb.env mind in
let cstrs = get_constructors pb.env indf in
let arsign, _ = get_arity pb.env indf in
let eqns,onlydflt = group_equations pb (fst mind) current cstrs pb.mat in
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 35a9cbdb2..bed77e622 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -45,6 +45,15 @@ let mkLambda_string s t c = mkLambda (Name (Id.of_string s), t, c)
(* Building curryfied elimination *)
(*******************************************)
+let is_private mib =
+ match mib.mind_private with
+ | Some true -> true
+ | _ -> false
+
+let check_privacy_block mib =
+ if is_private mib then
+ errorlabstrm ""(str"case analysis on a private inductive type")
+
(**********************************************************************)
(* Building case analysis schemes *)
(* Christine Paulin, 1996 *)
@@ -54,12 +63,13 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
let lnamespar = Vars.subst_univs_context usubst
mib.mind_params_ctxt
in
-
- if not (Sorts.List.mem kind (elim_sorts specif)) then
- raise
- (RecursionSchemeError
- (NotAllowedCaseAnalysis (false, fst (Universes.fresh_sort_in_family env kind), pind)));
-
+ let () = check_privacy_block mib in
+ let () =
+ if not (Sorts.List.mem kind (elim_sorts specif)) then
+ raise
+ (RecursionSchemeError
+ (NotAllowedCaseAnalysis (false, fst (Universes.fresh_sort_in_family env kind), pind)))
+ in
let ndepar = mip.mind_nrealargs_ctxt + 1 in
(* Pas génant car env ne sert pas à typer mais juste à renommer les Anonym *)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index da4595254..383d23306 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1093,6 +1093,10 @@ let pattern_occs loccs_trm env sigma c =
(* Used in several tactics. *)
+let check_privacy env ind =
+ if (fst (Inductive.lookup_mind_specif env (fst ind))).Declarations.mind_private = Some true then
+ errorlabstrm "" (str "case analysis on a private type")
+ else ind
(* put t as t'=(x1:A1)..(xn:An)B with B an inductive definition of name name
return name, B and t' *)
@@ -1100,7 +1104,7 @@ let reduce_to_ind_gen allow_product env sigma t =
let rec elimrec env t l =
let t = hnf_constr env sigma t in
match kind_of_term (fst (decompose_app t)) with
- | Ind ind-> (ind, it_mkProd_or_LetIn t l)
+ | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t l)
| Prod (n,ty,t') ->
if allow_product then
elimrec (push_rel (n,None,ty) env) t' ((n,None,ty)::l)
@@ -1111,7 +1115,7 @@ let reduce_to_ind_gen allow_product env sigma t =
was partially the case between V5.10 and V8.1 *)
let t' = whd_betadeltaiota env sigma t in
match kind_of_term (fst (decompose_app t')) with
- | Ind ind-> (ind, it_mkProd_or_LetIn t' l)
+ | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t' l)
| _ -> errorlabstrm "" (str"Not an inductive product.")
in
elimrec env t []
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 5146cd345..5e4bc5c46 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -14,6 +14,7 @@ open Reductionops
open Pattern
open Globnames
open Locus
+open Univ
type reduction_tactic_error =
InvalidAbstraction of env * constr * (env * Type_errors.type_error)
@@ -106,3 +107,7 @@ val contextually : bool -> occurrences * constr_pattern ->
val e_contextually : bool -> occurrences * constr_pattern ->
(patvar_map -> e_reduction_function) -> e_reduction_function
+
+(** Returns the same inductive if it is allowed for pattern-matching
+ raises an error otherwise. **)
+val check_privacy : env -> inductive puniverses -> inductive puniverses
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index e2d237815..6d7e3c38d 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -627,7 +627,7 @@ let rec pr_vernac = function
hov 2
(pr_assumption_token (n > 1) stre ++ spc() ++
pr_ne_params_list pr_lconstr_expr l)
- | VernacInductive (f,i,l) ->
+ | VernacInductive (p,f,i,l) ->
let pr_constructor (coe,(id,c)) =
hov 2 (pr_lident id ++ str" " ++
(if coe then str":>" else str":") ++
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 7a30923c8..fcfd616f4 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -126,7 +126,7 @@ let rec classify_vernac e =
let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd l) l) in
VtSideff ids, VtLater
| VernacDefinition (_,(_,id),DefineBody _) -> VtSideff [id], VtLater
- | VernacInductive (_,_,l) ->
+ | VernacInductive (_,_,_,l) ->
let ids = List.map (fun (((_,(_,id)),_,_,_,cl),_) -> id :: match cl with
| Constructors l -> List.map (fun (_,((_,id),_)) -> id) l
| RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 57931f600..eb8d27f25 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -755,7 +755,8 @@ let descend_then sigma env head dirn =
try find_rectype env sigma (get_type_of env sigma head)
with Not_found ->
error "Cannot project on an inductive type derived from a dependency." in
- let (ind,_),_ = dest_ind_family indf in
+ let indp,_ = (dest_ind_family indf) in
+ let ind, _ = check_privacy env indp in
let (mib,mip) = lookup_mind_specif env ind in
let cstr = get_constructors env indf in
let dirn_nlams = cstr.(dirn-1).cs_nargs in
@@ -804,7 +805,8 @@ let construct_discriminator sigma env dirn c sort =
errorlabstrm "Equality.construct_discriminator"
(str "Cannot discriminate on inductive constructors with \
dependent types.") in
- let ((ind,_),_) = dest_ind_family indf in
+ let (indp,_) = dest_ind_family indf in
+ let ind, _ = check_privacy env indp in
let (mib,mip) = lookup_mind_specif env ind in
let (true_0,false_0,sort_0) = build_coq_True(),build_coq_False(),Prop Null in
let deparsign = make_arity_signature env true indf in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 3f2a51888..22830eb6d 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -412,7 +412,7 @@ let inductive_levels env evdref arities inds =
!evdref (Array.to_list levels') destarities sizes
in evdref := evd; arities
-let interp_mutual_inductive (paramsl,indl) notations poly finite =
+let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
check_all_names_different indl;
let env0 = Global.env() in
let evdref = ref Evd.(from_env env0) in
@@ -487,6 +487,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly finite =
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 = Evd.universe_context evd },
impls
@@ -535,7 +536,7 @@ let declare_mutual_inductive_with_eliminations isrecord mie impls =
constrimpls)
impls;
if_verbose msg_info (minductive_message names);
- declare_default_schemes mind;
+ if mie.mind_entry_private == None then declare_default_schemes mind;
mind
type one_inductive_impls =
@@ -545,10 +546,10 @@ type one_inductive_impls =
type one_inductive_expr =
lident * local_binder list * constr_expr option * constructor_expr list
-let do_mutual_inductive indl poly finite =
+let do_mutual_inductive indl poly prv finite =
let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in
(* Interpret the types *)
- let mie,impls = interp_mutual_inductive indl ntns poly finite in
+ let mie,impls = interp_mutual_inductive indl ntns poly prv finite in
(* Declare the mutual inductive block with its associated schemes *)
ignore (declare_mutual_inductive_with_eliminations UserVerbose mie impls);
(* Declare the possible notations of inductive types *)
diff --git a/toplevel/command.mli b/toplevel/command.mli
index d2e601edd..41cb5baa3 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -86,7 +86,8 @@ type one_inductive_impls =
Impargs.manual_implicits list (** for constrs *)
val interp_mutual_inductive :
- structured_inductive_expr -> decl_notation list -> polymorphic -> bool(*finite*) ->
+ structured_inductive_expr -> decl_notation list -> polymorphic ->
+ private_flag -> bool(*finite*) ->
mutual_inductive_entry * one_inductive_impls list
(** Registering a mutual inductive definition together with its
@@ -99,7 +100,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 -> bool -> unit
+ (one_inductive_expr * decl_notation list) list -> polymorphic ->
+ private_flag -> bool -> unit
(** {6 Fixpoints and cofixpoints} *)
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index e17038a4f..5d0bcd78b 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -102,5 +102,6 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
mind_entry_params = params';
mind_entry_inds = inds';
mind_entry_polymorphic = mib.mind_polymorphic;
+ mind_entry_private = mib.mind_private;
mind_entry_universes = univs
}
diff --git a/toplevel/record.ml b/toplevel/record.ml
index b144dfe43..56493bae8 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -340,6 +340,7 @@ let declare_structure finite infer poly ctx id idbuild paramimpls params arity f
mind_entry_finite = finite != CoFinite;
mind_entry_inds = [mie_ind];
mind_entry_polymorphic = poly;
+ mind_entry_private = None;
mind_entry_universes = ctx } in
let kn = Command.declare_mutual_inductive_with_eliminations KernelVerbose mie [(paramimpls,[])] in
let rsp = (kn,0) in (* This is ind path of idstruc *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index bb702f79f..ca31d1f2e 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -534,7 +534,7 @@ let vernac_record k poly finite infer struc binders sort nameopt cfs =
| _ -> ()) cfs);
ignore(Record.definition_structure (k,poly,finite,infer,struc,binders,cfs,const,sort))
-let vernac_inductive poly finite infer indl =
+let vernac_inductive poly lo finite infer indl =
if Dumpglob.dump () then
List.iter (fun (((coe,lid), _, _, _, cstrs), _) ->
match cstrs with
@@ -565,7 +565,7 @@ let vernac_inductive poly finite infer indl =
| _ -> Errors.error "Cannot handle mutually (co)inductive records."
in
let indl = List.map unpack indl in
- do_mutual_inductive indl poly (finite != CoFinite)
+ do_mutual_inductive indl poly lo (finite != CoFinite)
let vernac_fixpoint locality poly local l =
let local = enforce_locality_exp locality local in
@@ -1696,7 +1696,7 @@ let interp ?proof 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 (finite,infer,l) -> vernac_inductive poly finite infer l
+ | VernacInductive (priv,finite,infer,l) -> vernac_inductive poly priv finite infer 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.39.1) at 2024-06-07 22:20:04 +0000