aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/funind/indfun_common.ml2
-rw-r--r--tactics/declare.ml59
-rw-r--r--tactics/declare.mli2
-rw-r--r--vernac/comAssumption.ml2
-rw-r--r--vernac/declareDef.ml5
-rw-r--r--vernac/lemmas.ml6
6 files changed, 31 insertions, 45 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 58b0ead130..ca19116ef0 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -128,7 +128,7 @@ let save name const ?hook uctx scope kind =
let r = match scope with
| Discharge ->
let c = SectionLocalDef const in
- let _ = declare_variable ~name ~kind (Lib.cwd(), c) in
+ let () = declare_variable ~name ~kind (Lib.cwd(), c) in
VarRef name
| Global local ->
let kn = declare_constant ~name ~kind ~local (DefinitionEntry const) in
diff --git a/tactics/declare.ml b/tactics/declare.ml
index d93fcc0950..da3a119a79 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -314,18 +314,21 @@ type section_variable_entry =
type variable_declaration = DirPath.t * section_variable_entry
-let cache_variable (_,o) =
- match o with
- | Inl ctx -> Global.push_context_set false ctx
- | Inr (id,(path,d),kind) ->
+(* This object is only for things which iterate over objects to find
+ variables (only Prettyp.print_context AFAICT) *)
+let inVariable : unit -> obj =
+ declare_object { (default_object "VARIABLE") with
+ classify_function = (fun () -> Dispose)}
+
+let declare_variable ~name ~kind (path,d) =
(* Constr raisonne sur les noms courts *)
- if Decls.variable_exists id then
- raise (AlreadyDeclared (None, id));
+ if Decls.variable_exists name then
+ raise (AlreadyDeclared (None, name));
let impl,opaque,poly,univs = match d with (* Fails if not well-typed *)
| SectionLocalAssum {typ;univs;poly;impl} ->
- let () = Global.push_context_set poly univs in
- let () = Global.push_named_assum (id,typ) in
+ let () = declare_universe_context ~poly univs in
+ let () = Global.push_named_assum (name,typ) in
let impl = if impl then Decl_kinds.Implicit else Decl_kinds.Explicit in
impl, true, poly, univs
| SectionLocalDef (de) ->
@@ -337,47 +340,29 @@ let cache_variable (_,o) =
let eff = get_roles export eff in
let () = List.iter register_side_effect eff in
let poly, univs = match de.proof_entry_universes with
- | Monomorphic_entry uctx -> false, uctx
- | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
+ | Monomorphic_entry uctx -> false, uctx
+ | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
in
let univs = Univ.ContextSet.union uctx univs in
(* We must declare the universe constraints before type-checking the
term. *)
- let () = Global.push_context_set (not poly) univs in
+ let () = declare_universe_context ~poly univs in
let se = {
secdef_body = body;
secdef_secctx = de.proof_entry_secctx;
secdef_feedback = de.proof_entry_feedback;
secdef_type = de.proof_entry_type;
} in
- let () = Global.push_named_def (id, se) in
+ let () = Global.push_named_def (name, se) in
Decl_kinds.Explicit, de.proof_entry_opaque,
- poly, univs in
- Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty id) (GlobRef.VarRef id);
- add_section_variable ~name:id ~kind:impl ~poly univs;
- Decls.(add_variable_data id {path;opaque;univs;poly;kind})
-
-let discharge_variable (_,o) = match o with
- | 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 * Decls.logical_kind) union
-
-let inVariable : variable_obj -> obj =
- declare_object { (default_object "VARIABLE") with
- cache_function = cache_variable;
- discharge_function = discharge_variable;
- classify_function = (fun _ -> Dispose) }
-
-(* for initial declaration *)
-let declare_variable ~name ~kind obj =
- let oname = add_leaf name (inVariable (Inr (name,obj,kind))) in
+ poly, univs
+ in
+ Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name);
+ add_section_variable ~name ~kind:impl ~poly univs;
+ Decls.(add_variable_data name {path;opaque;univs;poly;kind});
+ add_anonymous_leaf (inVariable ());
Impargs.declare_var_implicits name;
- Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name);
- oname
+ Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name)
(** Declaration of inductive blocks *)
let declare_inductive_argument_scopes kn mie =
diff --git a/tactics/declare.mli b/tactics/declare.mli
index f2d23fb319..3edb3f29cd 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -36,7 +36,7 @@ val declare_variable
: name:variable
-> kind:Decls.logical_kind
-> variable_declaration
- -> Libobject.object_name
+ -> unit
(** Declaration of global constructions
i.e. Definition/Theorem/Axiom/Parameter/... *)
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 60086a7861..520df1c21e 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -52,7 +52,7 @@ match scope with
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 () = 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
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 4dcb3db63b..2aa96fa8ed 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -48,8 +48,9 @@ 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 _ : Libobject.object_name =
- declare_variable ~name ~kind:Decls.(IsDefinition kind) (Lib.cwd(), SectionLocalDef ce) in
+ let () =
+ declare_variable ~name ~kind:Decls.(IsDefinition kind) (Lib.cwd(), SectionLocalDef ce)
+ in
VarRef name
| Global local ->
let kn = declare_constant ~name ~local ~kind:Decls.(IsDefinition kind) (DefinitionEntry ce) in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index d0e2e0f935..d6ee0b96f2 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -266,7 +266,7 @@ let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i
| 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
+ let () = Declare.declare_variable ~name ~kind (Lib.cwd(),c) in
(VarRef name,impargs)
| Global local ->
let kind = Decls.(IsAssumption Conjectural) in
@@ -289,7 +289,7 @@ let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i
| Discharge ->
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
+ 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
@@ -499,7 +499,7 @@ let finish_proved env sigma idopt po info =
let r = match scope with
| Discharge ->
let c = Declare.SectionLocalDef const in
- let _ = Declare.declare_variable ~name ~kind (Lib.cwd(), c) in
+ let () = Declare.declare_variable ~name ~kind (Lib.cwd(), c) in
let () = if should_suggest
then Proof_using.suggest_variable (Global.env ()) name
in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:48:56 +0000