diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 9 | ||||
| -rw-r--r-- | toplevel/command.mli | 6 | ||||
| -rw-r--r-- | toplevel/discharge.ml | 1 | ||||
| -rw-r--r-- | toplevel/record.ml | 1 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 6 |
5 files changed, 14 insertions, 9 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 3f2a518886..22830eb6df 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 d2e601edd5..41cb5baa3b 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 e17038a4fe..5d0bcd78b6 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 b144dfe43c..56493bae81 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 bb702f79f7..ca31d1f2ed 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 |