aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/classes.ml6
-rw-r--r--vernac/comAssumption.ml6
-rw-r--r--vernac/comDefinition.ml1
-rw-r--r--vernac/comInductive.ml69
-rw-r--r--vernac/comInductive.mli25
-rw-r--r--vernac/comPrimitive.ml2
-rw-r--r--vernac/declareDef.ml7
-rw-r--r--vernac/declareDef.mli2
-rw-r--r--vernac/declareInd.ml214
-rw-r--r--vernac/declareInd.mli23
-rw-r--r--vernac/declareObl.ml3
-rw-r--r--vernac/declareUniv.ml110
-rw-r--r--vernac/declareUniv.mli17
-rw-r--r--vernac/declaremods.ml14
-rw-r--r--vernac/lemmas.ml4
-rw-r--r--vernac/locality.ml6
-rw-r--r--vernac/record.ml2
-rw-r--r--vernac/vernac.mllib2
-rw-r--r--vernac/vernacentries.ml18
19 files changed, 414 insertions, 117 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 0a8c4e6b0f..09866a75c9 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -210,7 +210,7 @@ let discharge_class (_,cl) =
in grs', discharge_rel_context subst 1 ctx @ ctx' in
try
let info = abs_context cl in
- let ctx = info.Lib.abstr_ctx in
+ let ctx = info.Section.abstr_ctx in
let ctx, subst = rel_of_variable_context ctx in
let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in
let context = discharge_context ctx (subst, usubst) cl.cl_context in
@@ -325,7 +325,7 @@ let declare_instance_constant info global imps ?hook name decl poly sigma term t
let entry = Declare.definition_entry ~types:termtype ~univs:uctx term in
let kn = Declare.declare_constant ~name ~kind (Declare.DefinitionEntry entry) in
Declare.definition_message name;
- Declare.declare_univ_binders (GlobRef.ConstRef kn) (Evd.universe_binders sigma);
+ DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) (Evd.universe_binders sigma);
instance_hook info global imps ?hook (GlobRef.ConstRef kn)
let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst name =
@@ -338,7 +338,7 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst nam
let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in
let cst = Declare.declare_constant ~name
~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in
- Declare.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma);
+ DeclareUniv.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma);
instance_hook pri global imps (GlobRef.ConstRef cst)
let declare_instance_program env sigma ~global ~poly id pri imps decl term termtype =
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 5ba8b0ab3c..e5db6146ca 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -69,7 +69,7 @@ let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name
let kn = Declare.declare_constant ~name ~local ~kind decl in
let gr = GlobRef.ConstRef kn in
let () = maybe_declare_manual_implicits false gr imps in
- let () = Declare.declare_univ_binders gr pl in
+ let () = DeclareUniv.declare_univ_binders gr pl in
let () = Declare.assumption_message name in
let env = Global.env () in
let sigma = Evd.from_env env in
@@ -217,7 +217,7 @@ let context_insection sigma ~poly ctx =
in
let entry = Declare.definition_entry ~univs ~types:t b in
let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge
- ~kind:Decls.Definition UnivNames.empty_binders entry []
+ ~kind:Decls.(IsDefinition Definition) UnivNames.empty_binders entry []
in
()
in
@@ -287,7 +287,7 @@ let context ~poly l =
name,b,t,impl)
ctx
in
- if Lib.sections_are_opened ()
+ if Global.sections_are_opened ()
then context_insection sigma ~poly ctx
else context_nosection sigma ~poly ctx
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 9745358ba2..5b3f15a08c 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -104,4 +104,5 @@ let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_o
let ce = check_definition ~program_mode def in
let uctx = Evd.evar_universe_context evd in
let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
+ let kind = Decls.IsDefinition kind in
ignore(DeclareDef.declare_definition ~name ~scope ~kind ?hook_data (Evd.universe_binders evd) ce imps)
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 98b869d72e..cee5b7c1f4 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -15,18 +15,15 @@ open Util
open Constr
open Context
open Environ
-open Declare
open Names
open Libnames
open Nameops
open Constrexpr
open Constrexpr_ops
open Constrintern
-open Impargs
open Reductionops
open Type_errors
open Pretyping
-open Indschemes
open Context.Rel.Declaration
open Entries
@@ -80,12 +77,6 @@ type structured_one_inductive_expr = {
ind_lc : (Id.t * constr_expr) list
}
-let minductive_message = function
- | [] -> user_err Pp.(str "No inductive definition.")
- | [x] -> (Id.print x ++ str " is defined")
- | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++
- spc () ++ str "are defined")
-
let check_all_names_different indl =
let ind_names = List.map (fun ind -> ind.ind_name) indl in
let cstr_names = List.map_append (fun ind -> List.map fst ind.ind_lc) indl in
@@ -541,62 +532,6 @@ let extract_mutual_inductive_declaration_components indl =
let indl = extract_inductive indl in
(params,indl), coes, List.flatten ntnl
-let is_recursive mie =
- let rec is_recursive_constructor lift typ =
- match Constr.kind typ with
- | Prod (_,arg,rest) ->
- not (EConstr.Vars.noccurn Evd.empty (* FIXME *) lift (EConstr.of_constr arg)) ||
- is_recursive_constructor (lift+1) rest
- | LetIn (na,b,t,rest) -> is_recursive_constructor (lift+1) rest
- | _ -> false
- in
- match mie.mind_entry_inds with
- | [ind] ->
- let nparams = List.length mie.mind_entry_params in
- List.exists (fun t -> is_recursive_constructor (nparams+1) t) ind.mind_entry_lc
- | _ -> false
-
-let warn_non_primitive_record =
- CWarnings.create ~name:"non-primitive-record" ~category:"record"
- (fun indsp ->
- (hov 0 (str "The record " ++ Nametab.pr_global_env Id.Set.empty (GlobRef.IndRef indsp) ++
- strbrk" could not be defined as a primitive record")))
-
-let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie pl impls =
- (* spiwack: raises an error if the structure is supposed to be non-recursive,
- but isn't *)
- begin match mie.mind_entry_finite with
- | Declarations.BiFinite when is_recursive mie ->
- if Option.has_some mie.mind_entry_record then
- user_err Pp.(str "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command.")
- else
- user_err Pp.(str ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command."))
- | _ -> ()
- end;
- let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
- let (_, kn), prim = declare_mind mie in
- let mind = Global.mind_of_delta_kn kn in
- if primitive_expected && not prim then warn_non_primitive_record (mind,0);
- Declare.declare_univ_binders (GlobRef.IndRef (mind,0)) pl;
- List.iteri (fun i (indimpls, constrimpls) ->
- let ind = (mind,i) in
- let gr = GlobRef.IndRef ind in
- maybe_declare_manual_implicits false gr indimpls;
- List.iteri
- (fun j impls ->
- maybe_declare_manual_implicits false
- (GlobRef.ConstructRef (ind, succ j)) impls)
- constrimpls)
- impls;
- Flags.if_verbose Feedback.msg_info (minductive_message names);
- if mie.mind_entry_private == None
- then declare_default_schemes mind;
- mind
-
-type one_inductive_impls =
- Impargs.manual_implicits (* for inds *) *
- Impargs.manual_implicits list (* for constrs *)
-
type uniform_inductive_flag =
| UniformParameters
| NonUniformParameters
@@ -607,7 +542,7 @@ let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uni
let indl = match uniform with UniformParameters -> (params, [], indl) | NonUniformParameters -> ([], params, indl) in
let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template udecl indl ntns ~cumulative ~poly ~private_ind finite in
(* Declare the mutual inductive block with its associated schemes *)
- ignore (declare_mutual_inductive_with_eliminations mie pl impls);
+ ignore (DeclareInd.declare_mutual_inductive_with_eliminations mie pl impls);
(* Declare the possible notations of inductive types *)
List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns;
(* Declare the coercions *)
@@ -652,3 +587,5 @@ let make_cases ind =
let consref = GlobRef.ConstructRef (ith_constructor_of_inductive ind (i + 1)) in
(Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l)
mip.mind_nf_lc []
+
+let declare_mutual_inductive_with_eliminations = DeclareInd.declare_mutual_inductive_with_eliminations
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 7587bd165f..067fb3d2ca 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -9,7 +9,6 @@
(************************************************************************)
open Names
-open Entries
open Vernacexpr
open Constrexpr
@@ -42,22 +41,18 @@ val do_mutual_inductive
val make_cases : Names.inductive -> string list list
+val declare_mutual_inductive_with_eliminations
+ : ?primitive_expected:bool
+ -> Entries.mutual_inductive_entry
+ -> UnivNames.universe_binders
+ -> DeclareInd.one_inductive_impls list
+ -> Names.MutInd.t
+ [@@ocaml.deprecated "Please use DeclareInd.declare_mutual_inductive_with_eliminations"]
+
(************************************************************************)
(** Internal API, exported for Record *)
(************************************************************************)
-(** Registering a mutual inductive definition together with its
- associated schemes *)
-
-type one_inductive_impls =
- Impargs.manual_implicits (* for inds *) *
- Impargs.manual_implicits list (* for constrs *)
-
-val declare_mutual_inductive_with_eliminations :
- ?primitive_expected:bool ->
- mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list ->
- MutInd.t
-
val should_auto_template : Id.t -> bool -> bool
(** [should_auto_template x b] is [true] when [b] is [true] and we
automatically use template polymorphism. [x] is the name of the
@@ -72,7 +67,3 @@ val template_polymorphism_candidate :
can be made parametric in its conclusion sort, if one is given.
If the [Template Check] flag is false we just check that the conclusion sort
is not small. *)
-
-val sign_level : Environ.env -> Evd.evar_map -> Constr.rel_declaration list -> Univ.Universe.t
-(** [sign_level env sigma ctx] computes the universe level of the context [ctx]
- as the [sup] of its individual assumptions, which should be well-typed in [env] and [sigma] *)
diff --git a/vernac/comPrimitive.ml b/vernac/comPrimitive.ml
index 06fafddafb..b66ff876d3 100644
--- a/vernac/comPrimitive.ml
+++ b/vernac/comPrimitive.ml
@@ -9,7 +9,7 @@
(************************************************************************)
let do_primitive id prim typopt =
- if Lib.sections_are_opened () then
+ if Global.sections_are_opened () then
CErrors.user_err Pp.(str "Declaring a primitive is not allowed in sections.");
if Dumpglob.dump () then Dumpglob.dump_definition id false "ax";
let env = Global.env () in
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 1926faaf0e..f044c025d8 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -48,13 +48,13 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
let gr = match scope with
| Discharge ->
let () =
- declare_variable ~name ~kind:Decls.(IsDefinition kind) (SectionLocalDef ce)
+ declare_variable ~name ~kind (SectionLocalDef ce)
in
Names.GlobRef.VarRef name
| Global local ->
- let kn = declare_constant ~name ~local ~kind:Decls.(IsDefinition kind) (DefinitionEntry ce) in
+ let kn = declare_constant ~name ~local ~kind (DefinitionEntry ce) in
let gr = Names.GlobRef.ConstRef kn in
- let () = Declare.declare_univ_binders gr udecl in
+ let () = DeclareUniv.declare_univ_binders gr udecl in
gr
in
let () = maybe_declare_manual_implicits false gr imps in
@@ -69,6 +69,7 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
let declare_fix ?(opaque = false) ?hook_data ~name ~scope ~kind udecl univs ((def,_),eff) t imps =
let ce = definition_entry ~opaque ~types:t ~univs ~eff def in
+ let kind = Decls.IsDefinition kind in
declare_definition ~name ~scope ~kind ?hook_data udecl ce imps
let check_definition_evars ~allow_evars sigma =
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 54a0c9a7e8..d6001f5970 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -42,7 +42,7 @@ end
val declare_definition
: name:Id.t
-> scope:locality
- -> kind:Decls.definition_object_kind
+ -> kind:Decls.logical_kind
-> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
-> UnivNames.universe_binders
-> Evd.side_effects Declare.proof_entry
diff --git a/vernac/declareInd.ml b/vernac/declareInd.ml
new file mode 100644
index 0000000000..2375028541
--- /dev/null
+++ b/vernac/declareInd.ml
@@ -0,0 +1,214 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Names
+open Entries
+
+(** Declaration of inductive blocks *)
+let declare_inductive_argument_scopes kn mie =
+ List.iteri (fun i {mind_entry_consnames=lc} ->
+ Notation.declare_ref_arguments_scope Evd.empty (GlobRef.IndRef (kn,i));
+ for j=1 to List.length lc do
+ Notation.declare_ref_arguments_scope Evd.empty (GlobRef.ConstructRef ((kn,i),j));
+ done) mie.mind_entry_inds
+
+type inductive_obj = {
+ ind_names : (Id.t * Id.t list) list
+ (* For each block, name of the type + name of constructors *)
+}
+
+let inductive_names sp kn obj =
+ let (dp,_) = Libnames.repr_path sp in
+ let kn = Global.mind_of_delta_kn kn in
+ let names, _ =
+ List.fold_left
+ (fun (names, n) (typename, consnames) ->
+ let ind_p = (kn,n) in
+ let names, _ =
+ List.fold_left
+ (fun (names, p) l ->
+ let sp =
+ Libnames.make_path dp l
+ in
+ ((sp, GlobRef.ConstructRef (ind_p,p)) :: names, p+1))
+ (names, 1) consnames in
+ let sp = Libnames.make_path dp typename
+ in
+ ((sp, GlobRef.IndRef ind_p) :: names, n+1))
+ ([], 0) obj.ind_names
+ in names
+
+let load_inductive i ((sp, kn), names) =
+ let names = inductive_names sp kn names in
+ List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names
+
+let open_inductive i ((sp, kn), names) =
+ let names = inductive_names sp kn names in
+ List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names
+
+let cache_inductive ((sp, kn), names) =
+ let names = inductive_names sp kn names in
+ List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
+
+let discharge_inductive ((sp, kn), names) =
+ Some names
+
+let inInductive : inductive_obj -> Libobject.obj =
+ let open Libobject in
+ declare_object {(default_object "INDUCTIVE") with
+ cache_function = cache_inductive;
+ load_function = load_inductive;
+ open_function = open_inductive;
+ classify_function = (fun a -> Substitute a);
+ subst_function = ident_subst_function;
+ discharge_function = discharge_inductive;
+ }
+
+
+let cache_prim (_,(p,c)) = Recordops.register_primitive_projection p c
+
+let load_prim _ p = cache_prim p
+
+let subst_prim (subst,(p,c)) = Mod_subst.subst_proj_repr subst p, Mod_subst.subst_constant subst c
+
+let discharge_prim (_,(p,c)) = Some (Lib.discharge_proj_repr p, c)
+
+let inPrim : (Projection.Repr.t * Constant.t) -> Libobject.obj =
+ let open Libobject in
+ declare_object {
+ (default_object "PRIMPROJS") with
+ cache_function = cache_prim ;
+ load_function = load_prim;
+ subst_function = subst_prim;
+ classify_function = (fun x -> Substitute x);
+ discharge_function = discharge_prim }
+
+let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c))
+
+let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) =
+ let name = Label.to_id label in
+ let univs, u = match univs with
+ | Monomorphic_entry _ ->
+ (* Global constraints already defined through the inductive *)
+ Monomorphic_entry Univ.ContextSet.empty, Univ.Instance.empty
+ | Polymorphic_entry (nas, ctx) ->
+ Polymorphic_entry (nas, ctx), Univ.UContext.instance ctx
+ in
+ let term = Vars.subst_instance_constr u term in
+ let types = Vars.subst_instance_constr u types in
+ let entry = Declare.definition_entry ~types ~univs term in
+ let cst = Declare.declare_constant ~name ~kind:Decls.(IsDefinition StructureComponent) (Declare.DefinitionEntry entry) in
+ let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in
+ declare_primitive_projection p cst
+
+let declare_projections univs mind =
+ let env = Global.env () in
+ let mib = Environ.lookup_mind mind env in
+ let open Declarations in
+ match mib.mind_record with
+ | PrimRecord info ->
+ let iter_ind i (_, labs, _, _) =
+ let ind = (mind, i) in
+ let projs = Inductiveops.compute_projections env ind in
+ CArray.iter2_i (declare_one_projection univs ind ~proj_npars:mib.mind_nparams) labs projs
+ in
+ let () = Array.iteri iter_ind info in
+ true
+ | FakeRecord -> false
+ | NotRecord -> false
+
+let feedback_axiom () = Feedback.(feedback AddedAxiom)
+
+let is_unsafe_typing_flags () =
+ let open Declarations in
+ let flags = Environ.typing_flags (Global.env()) in
+ not (flags.check_universes && flags.check_guarded && flags.check_positive)
+
+(* for initial declaration *)
+let declare_mind mie =
+ let id = match mie.mind_entry_inds with
+ | ind::_ -> ind.mind_entry_typename
+ | [] -> CErrors.anomaly (Pp.str "cannot declare an empty list of inductives.") in
+ let map_names mip = (mip.mind_entry_typename, mip.mind_entry_consnames) in
+ let names = List.map map_names mie.mind_entry_inds in
+ List.iter (fun (typ, cons) ->
+ Declare.check_exists typ;
+ List.iter Declare.check_exists cons) names;
+ let _kn' = Global.add_mind id mie in
+ let (sp,kn as oname) = Lib.add_leaf id (inInductive { ind_names = names }) in
+ if is_unsafe_typing_flags() then feedback_axiom ();
+ let mind = Global.mind_of_delta_kn kn in
+ let isprim = declare_projections mie.mind_entry_universes mind in
+ Impargs.declare_mib_implicits mind;
+ declare_inductive_argument_scopes mind mie;
+ oname, isprim
+
+let is_recursive mie =
+ let open Constr in
+ let rec is_recursive_constructor lift typ =
+ match Constr.kind typ with
+ | Prod (_,arg,rest) ->
+ not (EConstr.Vars.noccurn Evd.empty (* FIXME *) lift (EConstr.of_constr arg)) ||
+ is_recursive_constructor (lift+1) rest
+ | LetIn (na,b,t,rest) -> is_recursive_constructor (lift+1) rest
+ | _ -> false
+ in
+ match mie.mind_entry_inds with
+ | [ind] ->
+ let nparams = List.length mie.mind_entry_params in
+ List.exists (fun t -> is_recursive_constructor (nparams+1) t) ind.mind_entry_lc
+ | _ -> false
+
+let warn_non_primitive_record =
+ CWarnings.create ~name:"non-primitive-record" ~category:"record"
+ (fun indsp ->
+ Pp.(hov 0 (str "The record " ++ Nametab.pr_global_env Id.Set.empty (GlobRef.IndRef indsp) ++
+ strbrk" could not be defined as a primitive record")))
+
+let minductive_message = function
+ | [] -> CErrors.user_err Pp.(str "No inductive definition.")
+ | [x] -> Pp.(Id.print x ++ str " is defined")
+ | l -> Pp.(hov 0 (prlist_with_sep pr_comma Id.print l ++
+ spc () ++ str "are defined"))
+
+type one_inductive_impls =
+ Impargs.manual_implicits (* for inds *) *
+ Impargs.manual_implicits list (* for constrs *)
+
+let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie pl impls =
+ (* spiwack: raises an error if the structure is supposed to be non-recursive,
+ but isn't *)
+ begin match mie.mind_entry_finite with
+ | Declarations.BiFinite when is_recursive mie ->
+ if Option.has_some mie.mind_entry_record then
+ CErrors.user_err Pp.(str "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command.")
+ else
+ CErrors.user_err Pp.(str ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command."))
+ | _ -> ()
+ end;
+ let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
+ let (_, kn), prim = declare_mind mie in
+ let mind = Global.mind_of_delta_kn kn in
+ if primitive_expected && not prim then warn_non_primitive_record (mind,0);
+ DeclareUniv.declare_univ_binders (GlobRef.IndRef (mind,0)) pl;
+ List.iteri (fun i (indimpls, constrimpls) ->
+ let ind = (mind,i) in
+ let gr = GlobRef.IndRef ind in
+ Impargs.maybe_declare_manual_implicits false gr indimpls;
+ List.iteri
+ (fun j impls ->
+ Impargs.maybe_declare_manual_implicits false
+ (GlobRef.ConstructRef (ind, succ j)) impls)
+ constrimpls)
+ impls;
+ Flags.if_verbose Feedback.msg_info (minductive_message names);
+ if mie.mind_entry_private == None
+ then Indschemes.declare_default_schemes mind;
+ mind
diff --git a/vernac/declareInd.mli b/vernac/declareInd.mli
new file mode 100644
index 0000000000..df8895a999
--- /dev/null
+++ b/vernac/declareInd.mli
@@ -0,0 +1,23 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(** Registering a mutual inductive definition together with its
+ associated schemes *)
+
+type one_inductive_impls =
+ Impargs.manual_implicits (* for inds *) *
+ Impargs.manual_implicits list (* for constrs *)
+
+val declare_mutual_inductive_with_eliminations
+ : ?primitive_expected:bool
+ -> Entries.mutual_inductive_entry
+ -> UnivNames.universe_binders
+ -> one_inductive_impls list
+ -> Names.MutInd.t
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 8fd6bc7eab..2c56f707f1 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -351,7 +351,8 @@ let declare_definition prg =
let ubinders = UState.universe_binders uctx in
let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in
DeclareDef.declare_definition
- ~name:prg.prg_name ~scope:prg.prg_scope ubinders ~kind:prg.prg_kind ce
+ ~name:prg.prg_name ~scope:prg.prg_scope ubinders
+ ~kind:Decls.(IsDefinition prg.prg_kind) ce
prg.prg_implicits ?hook_data
let rec lam_index n t acc =
diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml
new file mode 100644
index 0000000000..69ba9d76ec
--- /dev/null
+++ b/vernac/declareUniv.ml
@@ -0,0 +1,110 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Names
+
+type universe_source =
+ | BoundUniv (* polymorphic universe, bound in a function (this will go away someday) *)
+ | QualifiedUniv of Id.t (* global universe introduced by some global value *)
+ | UnqualifiedUniv (* other global universe *)
+
+type universe_name_decl = universe_source * (Id.t * Univ.Level.UGlobal.t) list
+
+let check_exists_universe sp =
+ if Nametab.exists_universe sp then
+ raise (Declare.AlreadyDeclared (Some "Universe", Libnames.basename sp))
+ else ()
+
+let qualify_univ i dp src id =
+ match src with
+ | BoundUniv | UnqualifiedUniv ->
+ i, Libnames.make_path dp id
+ | QualifiedUniv l ->
+ let dp = DirPath.repr dp in
+ Nametab.map_visibility succ i, Libnames.make_path (DirPath.make (l::dp)) id
+
+let do_univ_name ~check i dp src (id,univ) =
+ let i, sp = qualify_univ i dp src id in
+ if check then check_exists_universe sp;
+ Nametab.push_universe i sp univ
+
+let cache_univ_names ((sp, _), (src, univs)) =
+ let depth = Lib.sections_depth () in
+ let dp = Libnames.pop_dirpath_n depth (Libnames.dirpath sp) in
+ List.iter (do_univ_name ~check:true (Nametab.Until 1) dp src) univs
+
+let load_univ_names i ((sp, _), (src, univs)) =
+ List.iter (do_univ_name ~check:false (Nametab.Until i) (Libnames.dirpath sp) src) univs
+
+let open_univ_names i ((sp, _), (src, univs)) =
+ List.iter (do_univ_name ~check:false (Nametab.Exactly i) (Libnames.dirpath sp) src) univs
+
+let discharge_univ_names = function
+ | _, (BoundUniv, _) -> None
+ | _, ((QualifiedUniv _ | UnqualifiedUniv), _ as x) -> Some x
+
+let input_univ_names : universe_name_decl -> Libobject.obj =
+ let open Libobject in
+ declare_object
+ { (default_object "Global universe name state") with
+ cache_function = cache_univ_names;
+ load_function = load_univ_names;
+ open_function = open_univ_names;
+ discharge_function = discharge_univ_names;
+ subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a);
+ classify_function = (fun a -> Substitute a) }
+
+let declare_univ_binders gr pl =
+ if Global.is_polymorphic gr then
+ ()
+ else
+ let l = let open GlobRef in match gr with
+ | ConstRef c -> Label.to_id @@ Constant.label c
+ | IndRef (c, _) -> Label.to_id @@ MutInd.label c
+ | VarRef id ->
+ CErrors.anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".")
+ | ConstructRef _ ->
+ CErrors.anomaly ~label:"declare_univ_binders"
+ Pp.(str "declare_univ_binders on an constructor reference")
+ in
+ let univs = Id.Map.fold (fun id univ univs ->
+ match Univ.Level.name univ with
+ | None -> assert false (* having Prop/Set/Var as binders is nonsense *)
+ | Some univ -> (id,univ)::univs) pl []
+ in
+ Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs))
+
+let do_universe ~poly l =
+ let in_section = Global.sections_are_opened () in
+ let () =
+ if poly && not in_section then
+ CErrors.user_err ~hdr:"Constraint"
+ (Pp.str"Cannot declare polymorphic universes outside sections")
+ in
+ let l = List.map (fun {CAst.v=id} -> (id, UnivGen.new_univ_global ())) l in
+ let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx)
+ Univ.LSet.empty l, Univ.Constraint.empty
+ in
+ let src = if poly then BoundUniv else UnqualifiedUniv in
+ let () = Lib.add_anonymous_leaf (input_univ_names (src, l)) in
+ Declare.declare_universe_context ~poly ctx
+
+let do_constraint ~poly l =
+ let open Univ in
+ let u_of_id x =
+ Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x
+ in
+ let constraints = List.fold_left (fun acc (l, d, r) ->
+ let lu = u_of_id l and ru = u_of_id r in
+ Constraint.add (lu, d, ru) acc)
+ Constraint.empty l
+ in
+ let uctx = ContextSet.add_constraints constraints ContextSet.empty in
+ Declare.declare_universe_context ~poly uctx
diff --git a/vernac/declareUniv.mli b/vernac/declareUniv.mli
new file mode 100644
index 0000000000..ce2a6e225c
--- /dev/null
+++ b/vernac/declareUniv.mli
@@ -0,0 +1,17 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Names
+
+(** Global universe contexts, names and constraints *)
+val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit
+
+val do_universe : poly:bool -> lident list -> unit
+val do_constraint : poly:bool -> Glob_term.glob_constraint list -> unit
diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml
index 58a7dff5fd..c7b68d18c2 100644
--- a/vernac/declaremods.ml
+++ b/vernac/declaremods.ml
@@ -211,7 +211,7 @@ let compute_visibility exists i =
(** Iterate some function [iter_objects] on all components of a module *)
let do_module exists iter_objects i obj_dir obj_mp sobjs kobjs =
- let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in
+ let prefix = Nametab.{ obj_dir ; obj_mp; } in
let dirinfo = Nametab.GlobDirRef.DirModule prefix in
consistency_checks exists obj_dir dirinfo;
Nametab.push_dir (compute_visibility exists i) obj_dir dirinfo;
@@ -266,14 +266,14 @@ and load_objects i prefix objs =
and load_include i ((sp,kn), aobjs) =
let obj_dir = Libnames.dirpath sp in
let obj_mp = KerName.modpath kn in
- let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in
+ let prefix = Nametab.{ obj_dir; obj_mp; } in
let o = expand_aobjs aobjs in
load_objects i prefix o
and load_keep i ((sp,kn),kobjs) =
(* Invariant : seg isn't empty *)
let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in
- let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in
+ let prefix = Nametab.{ obj_dir ; obj_mp; } in
let modobjs =
try ModObjs.get obj_mp
with Not_found -> assert false (* a substobjs should already be loaded *)
@@ -327,7 +327,7 @@ let rec open_object i (name, obj) =
| KeepObject objs -> open_keep i (name, objs)
and open_module i obj_dir obj_mp sobjs =
- let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in
+ let prefix = Nametab.{ obj_dir ; obj_mp; } in
let dirinfo = Nametab.GlobDirRef.DirModule prefix in
consistency_checks true obj_dir dirinfo;
Nametab.push_dir (Nametab.Exactly i) obj_dir dirinfo;
@@ -353,7 +353,7 @@ and open_modtype i ((sp,kn),_) =
and open_include i ((sp,kn), aobjs) =
let obj_dir = Libnames.dirpath sp in
let obj_mp = KerName.modpath kn in
- let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in
+ let prefix = Nametab.{ obj_dir; obj_mp; } in
let o = expand_aobjs aobjs in
open_objects i prefix o
@@ -363,7 +363,7 @@ and open_export i mpl =
and open_keep i ((sp,kn),kobjs) =
let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in
- let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in
+ let prefix = Nametab.{ obj_dir; obj_mp; } in
open_objects i prefix kobjs
let rec cache_object (name, obj) =
@@ -380,7 +380,7 @@ let rec cache_object (name, obj) =
and cache_include ((sp,kn), aobjs) =
let obj_dir = Libnames.dirpath sp in
let obj_mp = KerName.modpath kn in
- let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in
+ let prefix = Nametab.{ obj_dir; obj_mp; } in
let o = expand_aobjs aobjs in
load_objects 1 prefix o;
open_objects 1 prefix o
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index e49277c51b..5ace8b917c 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -335,7 +335,7 @@ let finish_admitted env sigma ~name ~poly ~scope pe ctx hook ~udecl impargs othe
in
let kn = Declare.declare_constant ~name ~local ~kind:Decls.(IsAssumption Conjectural) (Declare.ParameterEntry pe) in
let () = Declare.assumption_message name in
- Declare.declare_univ_binders (GlobRef.ConstRef kn) (UState.universe_binders ctx);
+ DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) (UState.universe_binders ctx);
(* This takes care of the implicits and hook for the current constant*)
process_recthms ?fix_exn:None ?hook env sigma ctx ~udecl ~poly ~scope:(Global local) (GlobRef.ConstRef kn) impargs other_thms
@@ -425,7 +425,7 @@ let finish_proved env sigma idopt po info =
then Proof_using.suggest_constant (Global.env ()) kn
in
let gr = GlobRef.ConstRef kn in
- Declare.declare_univ_binders gr (UState.universe_binders universes);
+ DeclareUniv.declare_univ_binders gr (UState.universe_binders universes);
gr
in
Declare.definition_message name;
diff --git a/vernac/locality.ml b/vernac/locality.ml
index f033d32874..5862f51b43 100644
--- a/vernac/locality.ml
+++ b/vernac/locality.ml
@@ -39,7 +39,7 @@ let enforce_locality_exp locality_flag discharge =
match locality_flag, discharge with
| Some b, NoDischarge -> Global (importability_of_bool b)
| None, NoDischarge -> Global Declare.ImportDefaultBehavior
- | None, DoDischarge when not (Lib.sections_are_opened ()) ->
+ | None, DoDischarge when not (Global.sections_are_opened ()) ->
(* If a Let/Variable is defined outside a section, then we consider it as a local definition *)
warn_local_declaration ();
Global Declare.ImportNeedQualified
@@ -55,7 +55,7 @@ let enforce_locality locality_flag =
Local in sections is the default, Local not in section forces non-export *)
let make_section_locality =
- function Some b -> b | None -> Lib.sections_are_opened ()
+ function Some b -> b | None -> Global.sections_are_opened ()
let enforce_section_locality locality_flag =
make_section_locality locality_flag
@@ -68,7 +68,7 @@ let enforce_section_locality locality_flag =
let make_module_locality = function
| Some false ->
- if Lib.sections_are_opened () then
+ if Global.sections_are_opened () then
CErrors.user_err Pp.(str
"This command does not support the Global option in sections.");
false
diff --git a/vernac/record.ml b/vernac/record.ml
index 831fb53549..b60bfdfa22 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -466,7 +466,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
in
let mie = InferCumulativity.infer_inductive (Global.env ()) mie in
let impls = List.map (fun _ -> paramimpls, []) record_data in
- let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders impls
+ let kn = DeclareInd.declare_mutual_inductive_with_eliminations mie ubinders impls
~primitive_expected:!primitive_flag
in
let map i (_, _, _, _, fieldimpls, fields, is_coe, coers) =
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index afc701edbc..956b56e256 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -13,6 +13,7 @@ Ppvernac
Proof_using
Egramcoq
Metasyntax
+DeclareUniv
DeclareDef
DeclareObl
Canonical
@@ -28,6 +29,7 @@ ComDefinition
Classes
ComPrimitive
ComAssumption
+DeclareInd
ComInductive
ComFixpoint
ComProgramFixpoint
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4734ce1fb9..4ecd815dd2 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -810,18 +810,18 @@ let vernac_combined_scheme lid l =
Indschemes.do_combined_scheme lid l
let vernac_universe ~poly l =
- if poly && not (Lib.sections_are_opened ()) then
+ if poly && not (Global.sections_are_opened ()) then
user_err ~hdr:"vernac_universe"
(str"Polymorphic universes can only be declared inside sections, " ++
str "use Monomorphic Universe instead");
- Declare.do_universe ~poly l
+ DeclareUniv.do_universe ~poly l
let vernac_constraint ~poly l =
- if poly && not (Lib.sections_are_opened ()) then
+ if poly && not (Global.sections_are_opened ()) then
user_err ~hdr:"vernac_constraint"
(str"Polymorphic universe constraints can only be declared"
++ str " inside sections, use Monomorphic Constraint instead");
- Declare.do_constraint ~poly l
+ DeclareUniv.do_constraint ~poly l
(**********************)
(* Modules *)
@@ -837,7 +837,7 @@ let vernac_import export refl =
let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
(* We check the state of the system (in section, in module type)
and what module information is supplied *)
- if Lib.sections_are_opened () then
+ if Global.sections_are_opened () then
user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
let binders_ast = List.map
(fun (export,idl,ty) ->
@@ -852,7 +852,7 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mty_ast_o mexpr_ast_l =
(* We check the state of the system (in section, in module type)
and what module information is supplied *)
- if Lib.sections_are_opened () then
+ if Global.sections_are_opened () then
user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
match mexpr_ast_l with
| [] ->
@@ -893,7 +893,7 @@ let vernac_end_module export {loc;v=id} =
Option.iter (fun export -> vernac_import export [qualid_of_ident ?loc id]) export
let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l =
- if Lib.sections_are_opened () then
+ if Global.sections_are_opened () then
user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
match mty_ast_l with
@@ -969,7 +969,7 @@ let warn_require_in_section =
(fun () -> strbrk "Use of “Require” inside a section is deprecated.")
let vernac_require from import qidl =
- if Lib.sections_are_opened () then warn_require_in_section ();
+ if Global.sections_are_opened () then warn_require_in_section ();
let root = match from with
| None -> None
| Some from ->
@@ -2098,7 +2098,7 @@ let vernac_register qid r =
| RegisterCoqlib n ->
let ns, id = Libnames.repr_qualid n in
if DirPath.equal (dirpath_of_string "kernel") ns then begin
- if Lib.sections_are_opened () then
+ if Global.sections_are_opened () then
user_err Pp.(str "Registering a kernel type is not allowed in sections");
let pind = match Id.to_string id with
| "ind_bool" -> CPrimitives.PIT_bool
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 00:29:23 +0000