aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/funind/functional_principles_types.ml11
-rw-r--r--plugins/funind/indfun_common.ml18
-rw-r--r--plugins/funind/recdef.ml4
-rw-r--r--plugins/ltac/rewrite.ml17
-rw-r--r--plugins/setoid_ring/newring.ml6
-rw-r--r--tactics/abstract.ml4
-rw-r--r--tactics/declare.ml46
-rw-r--r--tactics/declare.mli43
-rw-r--r--tactics/hints.ml2
-rw-r--r--tactics/ind_tables.ml2
-rw-r--r--tactics/leminv.ml2
-rw-r--r--vernac/class.ml6
-rw-r--r--vernac/classes.ml15
-rw-r--r--vernac/comAssumption.ml36
-rw-r--r--vernac/comProgramFixpoint.ml2
-rw-r--r--vernac/declareDef.ml5
-rw-r--r--vernac/declareObl.ml5
-rw-r--r--vernac/indschemes.ml11
-rw-r--r--vernac/lemmas.ml98
-rw-r--r--vernac/obligations.ml4
-rw-r--r--vernac/record.ml12
21 files changed, 180 insertions, 169 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 87910eeae7..41db9796b9 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -369,9 +369,9 @@ let generate_functional_principle (evd: Evd.evar_map ref)
let ce = Declare.definition_entry ~univs value in
ignore(
Declare.declare_constant
- name
- (Declare.DefinitionEntry ce,
- Decls.(IsDefinition Scheme))
+ ~name
+ ~kind:Decls.(IsDefinition Scheme)
+ (Declare.DefinitionEntry ce)
);
Declare.definition_message name;
names := name :: !names
@@ -637,8 +637,9 @@ let build_scheme fas =
(fun (princ_id,_,_) def_entry ->
ignore
(Declare.declare_constant
- princ_id
- (Declare.DefinitionEntry def_entry,Decls.(IsProof Theorem)));
+ ~name:princ_id
+ ~kind:Decls.(IsProof Theorem)
+ (Declare.DefinitionEntry def_entry));
Declare.definition_message princ_id
)
fas
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index b32b27ebeb..17a96d0641 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -123,21 +123,21 @@ open DeclareDef
let definition_message = Declare.definition_message
-let save id const ?hook uctx scope kind =
+let save name const ?hook uctx scope kind =
let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in
let r = match scope with
| Discharge ->
- let k = Decls.logical_kind_of_goal_kind kind in
- let c = SectionLocalDef const in
- let _ = declare_variable id (Lib.cwd(), c, k) in
- VarRef id
+ let kind = Decls.logical_kind_of_goal_kind kind in
+ let c = SectionLocalDef const in
+ let _ = declare_variable ~name ~kind (Lib.cwd(), c) in
+ VarRef name
| Global local ->
- let k = Decls.logical_kind_of_goal_kind kind in
- let kn = declare_constant id ~local (DefinitionEntry const, k) in
- ConstRef kn
+ let kind = Decls.logical_kind_of_goal_kind kind in
+ let kn = declare_constant ~name ~kind ~local (DefinitionEntry const) in
+ ConstRef kn
in
DeclareDef.Hook.(call ?hook ~fix_exn { S.uctx; obls = []; scope; dref = r });
- definition_message id
+ definition_message name
let with_full_print f a =
let old_implicit_args = Impargs.is_implicit_args ()
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 0398acf242..a05feed1d1 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -65,9 +65,9 @@ let find_reference sl s =
let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in
locate (make_qualid dp (Id.of_string s))
-let declare_fun f_id kind ?univs value =
+let declare_fun name kind ?univs value =
let ce = definition_entry ?univs value (*FIXME *) in
- ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
+ ConstRef(declare_constant ~name ~kind (DefinitionEntry ce))
let defined lemma =
Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 22ad75b784..bef0dcc189 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1898,11 +1898,11 @@ let declare_projection n instance_id r =
let univs = Evd.univ_entry ~poly sigma in
let typ = EConstr.to_constr sigma typ in
let term = EConstr.to_constr sigma term in
- let cst =
- Declare.definition_entry ~types:typ ~univs term
- in
- ignore(Declare.declare_constant n
- (Declare.DefinitionEntry cst, Decls.(IsDefinition Definition)))
+ let cst = Declare.definition_entry ~types:typ ~univs term in
+ let _ : Constant.t =
+ Declare.declare_constant ~name:n ~kind:Decls.(IsDefinition Definition)
+ (Declare.DefinitionEntry cst)
+ in ()
let build_morphism_signature env sigma m =
let m,ctx = Constrintern.interp_constr env sigma m in
@@ -1978,10 +1978,9 @@ let add_morphism_as_parameter atts m n : unit =
let evd = Evd.from_env env in
let uctx, instance = build_morphism_signature env evd m in
let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in
- let cst = Declare.declare_constant instance_id
- (Declare.ParameterEntry
- (None,(instance,uctx),None),
- Decls.(IsAssumption Logical))
+ let cst = Declare.declare_constant ~name:instance_id
+ ~kind:Decls.(IsAssumption Logical)
+ (Declare.ParameterEntry (None,(instance,uctx),None))
in
Classes.add_instance (Classes.mk_instance
(PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst));
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 3d6bfda0b2..9973f2ec1d 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -155,9 +155,9 @@ let decl_constant na univs c =
let () = Declare.declare_universe_context ~poly:false univs in
let types = (Typeops.infer (Global.env ()) c).uj_type in
let univs = Monomorphic_entry Univ.ContextSet.empty in
- mkConst(declare_constant (Id.of_string na)
- (DefinitionEntry (definition_entry ~opaque:true ~types ~univs c),
- Decls.(IsProof Lemma)))
+ mkConst(declare_constant ~name:(Id.of_string na)
+ ~kind:Decls.(IsProof Lemma)
+ (DefinitionEntry (definition_entry ~opaque:true ~types ~univs c)))
(* Calling a global tactic *)
let ltac_call tac (args:glob_tactic_arg list) =
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 56f432ee1d..09d7e0278a 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -152,12 +152,12 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
let const, args = shrink_entry sign const in
let args = List.map EConstr.of_constr args in
let cd = Declare.DefinitionEntry { const with Proof_global.proof_entry_opaque = opaque } in
- let decl = (cd, if opaque then Decls.(IsProof Lemma) else Decls.(IsDefinition Definition)) in
+ let kind = if opaque then Decls.(IsProof Lemma) else Decls.(IsDefinition Definition) in
let cst () =
(* do not compute the implicit arguments, it may be costly *)
let () = Impargs.make_implicit_args false in
(* ppedrot: seems legit to have abstracted subproofs as local*)
- Declare.declare_private_constant ~local:Declare.ImportNeedQualified name decl
+ Declare.declare_private_constant ~local:Declare.ImportNeedQualified ~name ~kind cd
in
let cst, eff = Impargs.with_implicit_protection cst () in
let inst = match const.Proof_global.proof_entry_universes with
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 6a7f728abc..1e87a4b6ac 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -44,8 +44,6 @@ type 'a constant_entry =
| ParameterEntry of parameter_entry
| PrimitiveEntry of primitive_entry
-type constant_declaration = Evd.side_effects constant_entry * Decls.logical_kind
-
(* At load-time, the segment starting from the module name to the discharge *)
(* section (if Remark or Fact) is needed to access a construction *)
let load_constant i ((sp,kn), obj) =
@@ -235,7 +233,7 @@ let get_roles export eff =
in
List.map map export
-let define_constant ~side_effect id cd =
+let define_constant ~side_effect ~name cd =
let open Proof_global in
(* Logically define the constant and its subproofs, no libobject tampering *)
let is_poly de = match de.proof_entry_universes with
@@ -270,19 +268,19 @@ let define_constant ~side_effect id cd =
| PrimitiveEntry e ->
[], ConstantEntry (PureEntry, Entries.PrimitiveEntry e)
in
- let kn, eff = Global.add_constant ~side_effect ~in_section id decl in
+ let kn, eff = Global.add_constant ~side_effect ~in_section name decl in
kn, eff, export
-let declare_constant ?(local = ImportDefaultBehavior) id (cd, kind) =
- let () = check_exists id in
- let kn, (), export = define_constant ~side_effect:PureEntry id cd in
+let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd =
+ let () = check_exists name in
+ let kn, (), export = define_constant ~side_effect:PureEntry ~name cd in
(* Register the libobjects attached to the constants and its subproofs *)
let () = List.iter register_side_effect export in
let () = register_constant kn kind local in
kn
-let declare_private_constant ?role ?(local = ImportDefaultBehavior) id (cd, kind) =
- let kn, eff, export = define_constant ~side_effect:EffectEntry id cd in
+let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind cd =
+ let kn, eff, export = define_constant ~side_effect:EffectEntry ~name cd in
let () = assert (List.is_empty export) in
let () = register_constant kn kind local in
let seff_roles = match role with
@@ -294,24 +292,22 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) id (cd, kind
let declare_definition
?(opaque=false) ?(kind=Decls.Definition) ?(local = ImportDefaultBehavior)
- id ?types (body,univs) =
- let cb =
- definition_entry ?types ~univs ~opaque body
- in
- declare_constant ~local id
- (DefinitionEntry cb, Decls.IsDefinition kind)
+ ~name ?types (body,univs) =
+ let cb = definition_entry ?types ~univs ~opaque body in
+ declare_constant ~local ~name ~kind:Decls.(IsDefinition kind)
+ (DefinitionEntry cb)
(** Declaration of section variables and local definitions *)
type section_variable_entry =
| SectionLocalDef of Evd.side_effects Proof_global.proof_entry
| SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:bool }
-type variable_declaration = DirPath.t * section_variable_entry * Decls.logical_kind
+type variable_declaration = DirPath.t * section_variable_entry
let cache_variable ((sp,_),o) =
match o with
| Inl ctx -> Global.push_context_set false ctx
- | Inr (id,(path,d,kind)) ->
+ | Inr (id,(path,d),kind) ->
(* Constr raisonne sur les noms courts *)
if Decls.variable_exists id then
alreadydeclared (Id.print id ++ str " already exists");
@@ -351,13 +347,13 @@ let cache_variable ((sp,_),o) =
Decls.(add_variable_data id {path;opaque;univs;poly;kind})
let discharge_variable (_,o) = match o with
- | Inr (id,_) ->
+ | Inr (id,_,_) ->
if Decls.variable_polymorphic id then None
else Some (Inl (Decls.variable_context id))
| Inl _ -> Some o
type variable_obj =
- (Univ.ContextSet.t, Id.t * variable_declaration) union
+ (Univ.ContextSet.t, Id.t * variable_declaration * Decls.logical_kind) union
let inVariable : variable_obj -> obj =
declare_object { (default_object "VARIABLE") with
@@ -366,10 +362,10 @@ let inVariable : variable_obj -> obj =
classify_function = (fun _ -> Dispose) }
(* for initial declaration *)
-let declare_variable id obj =
- let oname = add_leaf id (inVariable (Inr (id,obj))) in
- declare_var_implicits id;
- Notation.declare_ref_arguments_scope Evd.empty (VarRef id);
+let declare_variable ~name ~kind obj =
+ let oname = add_leaf name (inVariable (Inr (name,obj,kind))) in
+ declare_var_implicits name;
+ Notation.declare_ref_arguments_scope Evd.empty (VarRef name);
oname
(** Declaration of inductive blocks *)
@@ -479,7 +475,7 @@ let inPrim : (Projection.Repr.t * Constant.t) -> obj =
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 id = Label.to_id label in
+ let name = Label.to_id label in
let univs, u = match univs with
| Monomorphic_entry _ ->
(* Global constraints already defined through the inductive *)
@@ -490,7 +486,7 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter
let term = Vars.subst_instance_constr u term in
let types = Vars.subst_instance_constr u types in
let entry = definition_entry ~types ~univs term in
- let cst = declare_constant id (DefinitionEntry entry, Decls.(IsDefinition StructureComponent)) in
+ let cst = declare_constant ~name ~kind:Decls.(IsDefinition StructureComponent) (DefinitionEntry entry) in
let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in
declare_primitive_projection p cst
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 0fc22f26c4..ae5c93db6a 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -30,15 +30,17 @@ type 'a constant_entry =
| ParameterEntry of parameter_entry
| PrimitiveEntry of primitive_entry
-type variable_declaration = DirPath.t * section_variable_entry * Decls.logical_kind
+type variable_declaration = DirPath.t * section_variable_entry
-val declare_variable : variable -> variable_declaration -> Libobject.object_name
+val declare_variable
+ : name:variable
+ -> kind:Decls.logical_kind
+ -> variable_declaration
+ -> Libobject.object_name
(** Declaration of global constructions
i.e. Definition/Theorem/Axiom/Parameter/... *)
-type constant_declaration = Evd.side_effects constant_entry * Decls.logical_kind
-
(* Default definition entries, transparent with no secctx or proj information *)
val definition_entry : ?fix_exn:Future.fix_exn ->
?opaque:bool -> ?inline:bool -> ?types:types ->
@@ -53,16 +55,29 @@ type import_status = ImportDefaultBehavior | ImportNeedQualified
internal specify if the constant has been created by the kernel or by the
user, and in the former case, if its errors should be silent *)
-val declare_constant :
- ?local:import_status -> Id.t -> constant_declaration -> Constant.t
-
-val declare_private_constant :
- ?role:Evd.side_effect_role -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects
-
-val declare_definition :
- ?opaque:bool -> ?kind:Decls.definition_object_kind ->
- ?local:import_status -> Id.t -> ?types:constr ->
- constr Entries.in_universes_entry -> Constant.t
+val declare_constant
+ : ?local:import_status
+ -> name:Id.t
+ -> kind:Decls.logical_kind
+ -> Evd.side_effects constant_entry
+ -> Constant.t
+
+val declare_private_constant
+ : ?role:Evd.side_effect_role
+ -> ?local:import_status
+ -> name:Id.t
+ -> kind:Decls.logical_kind
+ -> Evd.side_effects constant_entry
+ -> Constant.t * Evd.side_effects
+
+val declare_definition
+ : ?opaque:bool
+ -> ?kind:Decls.definition_object_kind
+ -> ?local:import_status
+ -> name:Id.t
+ -> ?types:constr
+ -> constr Entries.in_universes_entry
+ -> Constant.t
(** Since transparent constants' side effects are globally declared, we
* need that *)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 3a3a6b94dc..90c43a1cb4 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1320,7 +1320,7 @@ let project_hint ~poly pri l2r r =
in
let ctx = Evd.univ_entry ~poly sigma in
let c = EConstr.to_constr sigma c in
- let c = Declare.declare_definition id (c,ctx) in
+ let c = Declare.declare_definition ~name:id (c,ctx) in
let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
(info,false,true,PathAny, IsGlobRef (Globnames.ConstRef c))
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 29963bc105..e2ef05461b 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -135,7 +135,7 @@ let define internal role id c poly univs =
proof_entry_inline_code = false;
proof_entry_feedback = None;
} in
- let kn, eff = Declare.declare_private_constant ~role id (Declare.DefinitionEntry entry, Decls.(IsDefinition Scheme)) in
+ let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id (Declare.DefinitionEntry entry) in
let () = match internal with
| InternalTacticRequest -> ()
| _-> Declare.definition_message id
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 2ef06d2246..2af3947dd1 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -235,7 +235,7 @@ let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in
let univs = Evd.univ_entry ~poly sigma in
let entry = Declare.definition_entry ~univs invProof in
- let _ = Declare.declare_constant name (Declare.DefinitionEntry entry, Decls.(IsProof Lemma)) in
+ let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Lemma) (Declare.DefinitionEntry entry) in
()
(* inv_op = Inv (derives de complete inv. lemma)
diff --git a/vernac/class.ml b/vernac/class.ml
index c0d8837c2e..f79e459f43 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -207,7 +207,7 @@ let build_id_coercion idf_opt source poly =
user_err (strbrk
"Cannot be defined as coercion (maybe a bad number of arguments).")
in
- let idf =
+ let name =
match idf_opt with
| Some idf -> idf
| None ->
@@ -221,8 +221,8 @@ let build_id_coercion idf_opt source poly =
(definition_entry ~types:typ_f ~univs
~inline:true (mkCast (val_f, DEFAULTcast, typ_f)))
in
- let decl = (constr_entry, Decls.(IsDefinition IdentityCoercion)) in
- let kn = declare_constant idf decl in
+ let kind = Decls.(IsDefinition IdentityCoercion) in
+ let kn = declare_constant ~name ~kind constr_entry in
ConstRef kn
let check_source = function
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 01fc120af2..99a755e222 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -313,23 +313,22 @@ let instance_hook info global imps ?hook cst =
declare_instance env sigma (Some info) (not global) cst;
(match hook with Some h -> h cst | None -> ())
-let declare_instance_constant info global imps ?hook id decl poly sigma term termtype =
+let declare_instance_constant info global imps ?hook name decl poly sigma term termtype =
(* XXX: Duplication of the declare_constant path *)
- let kind = Decls.(IsDefinition Instance) in
let sigma =
let levels = Univ.LSet.union (CVars.universes_of_constr termtype)
(CVars.universes_of_constr term) in
Evd.restrict_universe_context sigma levels
in
let uctx = Evd.check_univ_decl ~poly sigma decl in
+ let kind = Decls.(IsDefinition Instance) in
let entry = Declare.definition_entry ~types:termtype ~univs:uctx term in
- let cdecl = (Declare.DefinitionEntry entry, kind) in
- let kn = Declare.declare_constant id cdecl in
- Declare.definition_message id;
+ let kn = Declare.declare_constant ~name ~kind (Declare.DefinitionEntry entry) in
+ Declare.definition_message name;
Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders sigma);
instance_hook info global imps ?hook (ConstRef kn)
-let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst id =
+let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst name =
let subst = List.fold_left2
(fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
[] subst (snd k.cl_context)
@@ -337,8 +336,8 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst id
let (_, ty_constr) = instance_constructor (k,u) subst in
let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in
- let cst = Declare.declare_constant id
- (Declare.ParameterEntry entry, Decls.(IsAssumption Logical)) in
+ let cst = Declare.declare_constant ~name
+ ~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in
Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma);
instance_hook pri global imps (ConstRef cst)
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index d7ad5133a6..60086a7861 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -42,7 +42,7 @@ let should_axiom_into_instance = let open Decls in function
true
| Definitional | Logical | Conjectural -> !axiom_into_instance
-let declare_assumption is_coe ~poly ~scope ~kind typ univs pl imps impl nl {CAst.v=ident} =
+let declare_assumption is_coe ~poly ~scope ~kind typ univs pl imps impl nl {CAst.v=name} =
let open DeclareDef in
match scope with
| Discharge ->
@@ -50,10 +50,11 @@ match scope with
| Monomorphic_entry univs -> univs
| Polymorphic_entry (_, univs) -> Univ.ContextSet.of_context univs
in
- let decl = (Lib.cwd(), SectionLocalAssum {typ;univs;poly;impl}, Decls.IsAssumption kind) in
- let _ = declare_variable ident decl in
- let () = assumption_message ident in
- let r = VarRef ident in
+ let kind = Decls.IsAssumption kind in
+ let decl = Lib.cwd(), SectionLocalAssum {typ; univs; poly; impl} in
+ let _ = declare_variable ~name ~kind decl in
+ let () = assumption_message name in
+ let r = VarRef name in
let () = maybe_declare_manual_implicits true r imps in
let env = Global.env () in
let sigma = Evd.from_env env in
@@ -68,12 +69,13 @@ match scope with
| DefaultInline -> Some (Flags.get_inline_level())
| InlineAt i -> Some i
in
- let decl = (Declare.ParameterEntry (None,(typ,univs),inl), Decls.IsAssumption kind) in
- let kn = declare_constant ident ~local decl in
+ let kind = Decls.IsAssumption kind in
+ let decl = Declare.ParameterEntry (None,(typ,univs),inl) in
+ let kn = declare_constant ~name ~local ~kind decl in
let gr = ConstRef kn in
let () = maybe_declare_manual_implicits false gr imps in
let () = Declare.declare_univ_binders gr pl in
- let () = assumption_message ident in
+ let () = assumption_message name in
let env = Global.env () in
let sigma = Evd.from_env env in
let () = if do_instance then Classes.declare_instance env sigma None false gr in
@@ -210,7 +212,8 @@ let do_primitive id prim typopt =
prim_entry_content = prim;
}
in
- let _kn = declare_constant id.CAst.v (PrimitiveEntry entry, Decls.IsPrimitive) in
+ let _kn : Names.Constant.t =
+ declare_constant ~name:id.CAst.v ~kind:Decls.IsPrimitive (PrimitiveEntry entry) in
Flags.if_verbose Feedback.msg_info Pp.(Id.print id.CAst.v ++ str " is declared")
let named_of_rel_context l =
@@ -268,24 +271,25 @@ let context ~poly l =
Monomorphic_entry Univ.ContextSet.empty
end
in
- let fn status (id, b, t) =
+ let fn status (name, b, t) =
let b, t = Option.map (EConstr.to_constr sigma) b, EConstr.to_constr sigma t in
if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
(* Declare the universe context once *)
+ let kind = Decls.(IsAssumption Logical) in
let decl = match b with
| None ->
- (Declare.ParameterEntry (None,(t,univs),None), Decls.(IsAssumption Logical))
+ Declare.ParameterEntry (None,(t,univs),None)
| Some b ->
let entry = Declare.definition_entry ~univs ~types:t b in
- (Declare.DefinitionEntry entry, Decls.(IsAssumption Logical))
+ Declare.DefinitionEntry entry
in
- let cst = Declare.declare_constant id decl in
+ let cst = Declare.declare_constant ~name ~kind decl in
let env = Global.env () in
Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (ConstRef cst);
status
else
let test x = match x.CAst.v with
- | Some (Name id',_) -> Id.equal id id'
+ | Some (Name id',_) -> Id.equal name id'
| _ -> false
in
let impl = List.exists test impls in
@@ -294,11 +298,11 @@ let context ~poly l =
let nstatus = match b with
| None ->
pi3 (declare_assumption false ~scope ~poly ~kind:Decls.Context t univs UnivNames.empty_binders [] impl
- Declaremods.NoInline (CAst.make id))
+ Declaremods.NoInline (CAst.make name))
| Some b ->
let entry = Declare.definition_entry ~univs ~types:t b in
let _gr = DeclareDef.declare_definition
- ~name:id ~scope:DeclareDef.Discharge
+ ~name ~scope:DeclareDef.Discharge
~kind:Decls.Definition UnivNames.empty_binders entry [] in
Lib.sections_are_opened () || Lib.is_modtype_strict ()
in
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 95f8fff520..4d663d6b0e 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -212,7 +212,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
(*FIXME poly? *)
let ce = definition_entry ~types:ty ~univs (EConstr.to_constr sigma body) in
(* FIXME: include locality *)
- let c = Declare.declare_constant recname (DefinitionEntry ce, Decls.(IsDefinition Definition)) in
+ let c = Declare.declare_constant ~name:recname ~kind:Decls.(IsDefinition Definition) (DefinitionEntry ce) in
let gr = ConstRef c in
if Impargs.is_implicit_args () || not (List.is_empty impls) then
Impargs.declare_manual_implicits false gr impls
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 7487c99f56..4dcb3db63b 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -48,10 +48,11 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
let fix_exn = Future.fix_exn_of ce.Proof_global.proof_entry_body in
let gr = match scope with
| Discharge ->
- let _ = declare_variable name (Lib.cwd(), SectionLocalDef ce, Decls.IsDefinition kind) in
+ let _ : Libobject.object_name =
+ declare_variable ~name ~kind:Decls.(IsDefinition kind) (Lib.cwd(), SectionLocalDef ce) in
VarRef name
| Global local ->
- let kn = declare_constant name ~local (DefinitionEntry ce, Decls.IsDefinition kind) in
+ let kn = declare_constant ~name ~local ~kind:Decls.(IsDefinition kind) (DefinitionEntry ce) in
let gr = ConstRef kn in
let () = Declare.declare_univ_binders gr udecl in
gr
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 0ab02862f0..a947fa2668 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -166,8 +166,9 @@ let declare_obligation prg obl body ty uctx =
in
(* ppedrot: seems legit to have obligations as local *)
let constant =
- Declare.declare_constant obl.obl_name ~local:Declare.ImportNeedQualified
- (Declare.DefinitionEntry ce, Decls.(IsProof Property))
+ Declare.declare_constant ~name:obl.obl_name
+ ~local:Declare.ImportNeedQualified ~kind:Decls.(IsProof Property)
+ (Declare.DefinitionEntry ce)
in
if not opaque then
add_hint (Locality.make_section_locality None) prg constant;
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 26499ce994..0ee15bde6e 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -99,11 +99,11 @@ let () =
(* Util *)
-let define ~poly id sigma c t =
- let f = declare_constant in
+let define ~poly name sigma c t =
+ let f = declare_constant ~kind:Decls.(IsDefinition Scheme) in
let univs = Evd.univ_entry ~poly sigma in
let open Proof_global in
- let kn = f id
+ let kn = f ~name
(DefinitionEntry
{ proof_entry_body = c;
proof_entry_secctx = None;
@@ -112,9 +112,8 @@ let define ~poly id sigma c t =
proof_entry_opaque = false;
proof_entry_inline_code = false;
proof_entry_feedback = None;
- },
- Decls.(IsDefinition Scheme)) in
- definition_message id;
+ }) in
+ definition_message name;
kn
(* Boolean equality *)
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 2908481dea..226697a29a 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -21,8 +21,6 @@ open Declareops
open Entries
open Nameops
open Globnames
-open Decls
-open Declare
open Pretyping
open Termops
open Reductionops
@@ -77,7 +75,8 @@ module Info = struct
; kind : Decls.goal_object_kind
}
- let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Proof Lemma) () =
+ let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior)
+ ?(kind=Decls.(Proof Lemma)) () =
{ hook
; compute_guard = []
; impargs = []
@@ -120,14 +119,15 @@ let by tac pf =
let retrieve_first_recthm uctx = function
| VarRef id ->
- (NamedDecl.get_value (Global.lookup_named id),variable_opacity id)
+ NamedDecl.get_value (Global.lookup_named id),
+ Decls.variable_opacity id
| ConstRef cst ->
- let cb = Global.lookup_constant cst in
- (* we get the right order somehow but surely it could be enforced in a better way *)
- let uctx = UState.context uctx in
- let inst = Univ.UContext.instance uctx in
- let map (c, _, _) = Vars.subst_instance_constr inst c in
- (Option.map map (Global.body_of_constant_body Library.indirect_accessor cb), is_opaque cb)
+ let cb = Global.lookup_constant cst in
+ (* we get the right order somehow but surely it could be enforced in a better way *)
+ let uctx = UState.context uctx in
+ let inst = Univ.UContext.instance uctx in
+ let map (c, _, _) = Vars.subst_instance_constr inst c in
+ (Option.map map (Global.body_of_constant_body Library.indirect_accessor cb), is_opaque cb)
| _ -> assert false
let adjust_guardness_conditions const = function
@@ -252,27 +252,27 @@ let check_name_freshness locality {CAst.loc;v=id} : unit =
let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i
{ Recthm.name; typ; impargs } =
let t_i = norm typ in
- let k = IsAssumption Conjectural in
+ let kind = Decls.(IsAssumption Conjectural) in
match body with
| None ->
let open DeclareDef in
(match scope with
| Discharge ->
- let impl = false in (* copy values from Vernacentries *)
- let univs = match univs with
- | Polymorphic_entry (_, univs) ->
- (* What is going on here? *)
- Univ.ContextSet.of_context univs
- | Monomorphic_entry univs -> univs
- in
- let c = SectionLocalAssum {typ=t_i;univs;poly;impl} in
- let _ = declare_variable name (Lib.cwd(),c,k) in
- (VarRef name,impargs)
+ let impl = false in (* copy values from Vernacentries *)
+ let univs = match univs with
+ | Polymorphic_entry (_, univs) ->
+ (* What is going on here? *)
+ Univ.ContextSet.of_context univs
+ | Monomorphic_entry univs -> univs
+ in
+ let c = Declare.SectionLocalAssum {typ=t_i; univs; poly; impl} in
+ let _ = Declare.declare_variable ~name ~kind (Lib.cwd(),c) in
+ (VarRef name,impargs)
| Global local ->
- let k = IsAssumption Conjectural in
- let decl = (ParameterEntry (None,(t_i,univs),None), k) in
- let kn = declare_constant name ~local decl in
- (ConstRef kn,impargs))
+ let kind = Decls.(IsAssumption Conjectural) in
+ let decl = Declare.ParameterEntry (None,(t_i,univs),None) in
+ let kn = Declare.declare_constant ~name ~local ~kind decl in
+ (ConstRef kn,impargs))
| Some body ->
let body = norm body in
let rec body_i t = match Constr.kind t with
@@ -287,15 +287,13 @@ let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i
let open DeclareDef in
match scope with
| Discharge ->
- let const = definition_entry ~types:t_i ~opaque:opaq ~univs body_i in
- let c = SectionLocalDef const in
- let _ = declare_variable name (Lib.cwd(), c, k) in
- (VarRef name,impargs)
+ let const = Declare.definition_entry ~types:t_i ~opaque:opaq ~univs body_i in
+ let c = Declare.SectionLocalDef const in
+ let _ = Declare.declare_variable ~name ~kind (Lib.cwd(), c) in
+ (VarRef name,impargs)
| Global local ->
- let const =
- Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i
- in
- let kn = declare_constant name ~local (DefinitionEntry const, k) in
+ let const = Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i in
+ let kn = Declare.declare_constant ~name ~local ~kind (Declare.DefinitionEntry const) in
(ConstRef kn,impargs)
let initialize_named_context_for_proof () =
@@ -303,7 +301,7 @@ let initialize_named_context_for_proof () =
List.fold_right
(fun d signv ->
let id = NamedDecl.get_id d in
- let d = if variable_opacity id then NamedDecl.drop_body d else d in
+ let d = if Decls.variable_opacity id then NamedDecl.drop_body d else d in
Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
(* Starting a goal *)
@@ -445,10 +443,10 @@ let finish_admitted env sigma ~name ~poly ~scope pe ctx hook ~udecl impargs othe
let open DeclareDef in
let local = match scope with
| Global local -> local
- | Discharge -> warn_let_as_axiom name; ImportNeedQualified
+ | Discharge -> warn_let_as_axiom name; Declare.ImportNeedQualified
in
- let kn = declare_constant name ~local (ParameterEntry pe, IsAssumption Conjectural) in
- let () = assumption_message name 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 (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) (ConstRef kn) impargs other_thms;
@@ -496,20 +494,20 @@ let finish_proved env sigma idopt po info =
let fix_exn = Future.fix_exn_of const.proof_entry_body in
let () = try
let const = adjust_guardness_conditions const compute_guard in
- let k = Decls.logical_kind_of_goal_kind kind in
+ let kind = Decls.logical_kind_of_goal_kind kind in
let should_suggest = const.proof_entry_opaque && Option.is_empty const.proof_entry_secctx in
let open DeclareDef in
let r = match scope with
| Discharge ->
- let c = SectionLocalDef const in
- let _ = declare_variable name (Lib.cwd(), c, k) in
+ let c = Declare.SectionLocalDef const in
+ let _ = Declare.declare_variable ~name ~kind (Lib.cwd(), c) in
let () = if should_suggest
then Proof_using.suggest_variable (Global.env ()) name
in
VarRef name
| Global local ->
let kn =
- declare_constant name ~local (DefinitionEntry const, k) in
+ Declare.declare_constant ~name ~local ~kind (Declare.DefinitionEntry const) in
let () = if should_suggest
then Proof_using.suggest_constant (Global.env ()) kn
in
@@ -517,7 +515,7 @@ let finish_proved env sigma idopt po info =
Declare.declare_univ_binders gr (UState.universe_binders universes);
gr
in
- definition_message name;
+ Declare.definition_message name;
(* This takes care of the implicits and hook for the current constant*)
process_recthms ~fix_exn ?hook env sigma universes ~udecl ~poly ~scope r impargs other_thms
with e when CErrors.noncritical e ->
@@ -542,8 +540,9 @@ let finish_derived ~f ~name ~idopt ~entries =
(* The opacity of [f_def] is adjusted to be [false], as it
must. Then [f] is declared in the global environment. *)
let f_def = { f_def with Proof_global.proof_entry_opaque = false } in
- let f_def = Declare.DefinitionEntry f_def , IsDefinition Definition in
- let f_kn = Declare.declare_constant f f_def in
+ let f_kind = Decls.(IsDefinition Definition) in
+ let f_def = Declare.DefinitionEntry f_def in
+ let f_kn = Declare.declare_constant ~name:f ~kind:f_kind f_def in
let f_kn_term = mkConst f_kn in
(* In the type and body of the proof of [suchthat] there can be
references to the variable [f]. It needs to be replaced by
@@ -565,17 +564,14 @@ let finish_derived ~f ~name ~idopt ~entries =
proof_entry_body = lemma_body;
proof_entry_type = Some lemma_type }
in
- let lemma_def =
- Declare.DefinitionEntry lemma_def ,
- Decls.(IsProof Proposition)
- in
- let _ : Names.Constant.t = Declare.declare_constant name lemma_def in
+ let lemma_def = Declare.DefinitionEntry lemma_def in
+ let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in
()
let finish_proved_equations lid kind proof_obj hook i types wits sigma0 =
let obls = ref 1 in
- let kind = match kind with
+ let kind = let open Decls in match kind with
| DefinitionBody d -> IsDefinition d
| Proof p -> IsProof p
in
@@ -587,7 +583,7 @@ let finish_proved_equations lid kind proof_obj hook i types wits sigma0 =
| None -> let n = !obls in incr obls; add_suffix i ("_obligation_" ^ string_of_int n)
in
let entry, args = Abstract.shrink_entry local_context entry in
- let cst = Declare.declare_constant id (Declare.DefinitionEntry entry, kind) in
+ let cst = Declare.declare_constant ~name:id ~kind (Declare.DefinitionEntry entry) in
let sigma, app = Evarutil.new_global sigma (ConstRef cst) in
let sigma = Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma in
sigma, cst) sigma0
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 92adad2299..7e615c05b0 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -688,8 +688,8 @@ let admit_prog prg =
| None ->
let x = subst_deps_obl obls x in
let ctx = UState.univ_entry ~poly:false prg.prg_ctx in
- let kn = Declare.declare_constant x.obl_name ~local:Declare.ImportNeedQualified
- (Declare.ParameterEntry (None,(x.obl_type,ctx),None), Decls.(IsAssumption Conjectural))
+ let kn = Declare.declare_constant ~name:x.obl_name ~local:Declare.ImportNeedQualified
+ (Declare.ParameterEntry (None,(x.obl_type,ctx),None)) ~kind:Decls.(IsAssumption Conjectural)
in
assumption_message x.obl_name;
obls.(i) <- { x with obl_body = Some (DefinedObl (kn, Univ.Instance.empty)) }
diff --git a/vernac/record.ml b/vernac/record.ml
index 08239eb544..7c29130383 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -351,8 +351,8 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
proof_entry_opaque = false;
proof_entry_inline_code = false;
proof_entry_feedback = None } in
- let k = (Declare.DefinitionEntry entry,Decls.IsDefinition kind) in
- let kn = declare_constant fid k in
+ let kind = Decls.IsDefinition kind in
+ let kn = declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry) in
let constr_fip =
let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
applist (mkConstU (kn,u),proj_args)
@@ -496,8 +496,8 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
let class_type = it_mkProd_or_LetIn arity params in
let class_entry =
Declare.definition_entry ~types:class_type ~univs class_body in
- let cst = Declare.declare_constant id
- (DefinitionEntry class_entry, Decls.(IsDefinition Definition))
+ let cst = Declare.declare_constant ~name:id
+ (DefinitionEntry class_entry) ~kind:Decls.(IsDefinition Definition)
in
let inst, univs = match univs with
| Polymorphic_entry (_, uctx) -> Univ.UContext.instance uctx, univs
@@ -511,8 +511,8 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
let proj_body =
it_mkLambda_or_LetIn (mkLambda (binder, inst_type, mkRel 1)) params in
let proj_entry = Declare.definition_entry ~types:proj_type ~univs proj_body in
- let proj_cst = Declare.declare_constant proj_name
- (DefinitionEntry proj_entry, Decls.(IsDefinition Definition))
+ let proj_cst = Declare.declare_constant ~name:proj_name
+ (DefinitionEntry proj_entry) ~kind:Decls.(IsDefinition Definition)
in
let cref = ConstRef cst in
Impargs.declare_manual_implicits false cref paramimpls;
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:52:28 +0000