aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/base_include2
-rw-r--r--plugins/ltac/extratactics.mlg2
-rw-r--r--plugins/ltac/leminv.ml (renamed from tactics/leminv.ml)0
-rw-r--r--plugins/ltac/leminv.mli (renamed from tactics/leminv.mli)0
-rw-r--r--plugins/ltac/ltac_plugin.mlpack1
-rw-r--r--plugins/setoid_ring/newring.ml2
-rw-r--r--tactics/abstract.ml5
-rw-r--r--tactics/abstract.mli12
-rw-r--r--tactics/declareUctx.ml34
-rw-r--r--tactics/declareUctx.mli11
-rw-r--r--tactics/hints.ml5
-rw-r--r--tactics/hints.mli2
-rw-r--r--tactics/ind_tables.ml8
-rw-r--r--tactics/ind_tables.mli8
-rw-r--r--tactics/tactics.mllib3
-rw-r--r--vernac/comAssumption.ml6
-rw-r--r--vernac/comHints.ml2
-rw-r--r--vernac/declare.ml (renamed from tactics/declare.ml)37
-rw-r--r--vernac/declare.mli (renamed from tactics/declare.mli)15
-rw-r--r--vernac/declareUniv.ml4
-rw-r--r--vernac/vernac.mllib1
-rw-r--r--vernac/vernacentries.ml3
22 files changed, 101 insertions, 62 deletions
diff --git a/dev/base_include b/dev/base_include
index 96a867475d..45e79147c1 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -129,7 +129,7 @@ open Elim
open Equality
open Hipattern
open Inv
-open Leminv
+open Ltac_plugin.Leminv
open Tacticals
open Tactics
open Eqschemes
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 7754fe401e..0bad3cbe5b 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -312,7 +312,7 @@ let add_rewrite_hint ~poly bases ort t lcsr =
if poly then ctx
else (* This is a global universe context that shouldn't be
refreshed at every use of the hint, declare it globally. *)
- (Declare.declare_universe_context ~poly:false ctx;
+ (DeclareUctx.declare_universe_context ~poly:false ctx;
Univ.ContextSet.empty)
in
CAst.make ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in
diff --git a/tactics/leminv.ml b/plugins/ltac/leminv.ml
index 5a8ec404ee..5a8ec404ee 100644
--- a/tactics/leminv.ml
+++ b/plugins/ltac/leminv.ml
diff --git a/tactics/leminv.mli b/plugins/ltac/leminv.mli
index 5a5de7b58f..5a5de7b58f 100644
--- a/tactics/leminv.mli
+++ b/plugins/ltac/leminv.mli
diff --git a/plugins/ltac/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack
index e83eab20dc..f31361279c 100644
--- a/plugins/ltac/ltac_plugin.mlpack
+++ b/plugins/ltac/ltac_plugin.mlpack
@@ -9,6 +9,7 @@ Tactic_debug
Tacintern
Profile_ltac
Tactic_matching
+Leminv
Tacinterp
Tacentries
Evar_tactics
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 0646af3552..633cdbd735 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -150,7 +150,7 @@ let decl_constant na univs c =
let open Constr in
let vars = CVars.universes_of_constr c in
let univs = UState.restrict_universe_context ~lbound:(Global.universes_lbound ()) univs vars in
- let () = Declare.declare_universe_context ~poly:false univs in
+ let () = DeclareUctx.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 ~name:(Id.of_string na)
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 0e78a03f45..6b575d0807 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -40,6 +40,9 @@ let name_op_to_name ~name_op ~name suffix =
| Some s -> s
| None -> Nameops.add_suffix name suffix
+let declare_abstract = ref (fun ~name ~poly ~kind ~sign ~secsign ~opaque ~solve_tac sigma concl ->
+ CErrors.anomaly (Pp.str "Abstract declaration hook not registered"))
+
let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
let open Tacticals.New in
let open Tacmach.New in
@@ -77,7 +80,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
let concl = it_mkNamedProd_or_LetIn concl sign in
let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in
let effs, sigma, lem, args, safe =
- Declare.declare_abstract ~name ~poly ~sign ~secsign ~kind ~opaque ~solve_tac sigma concl in
+ !declare_abstract ~name ~poly ~sign ~secsign ~kind ~opaque ~solve_tac sigma concl in
let solve =
Proofview.tclEFFECTS effs <*>
tacK lem args
diff --git a/tactics/abstract.mli b/tactics/abstract.mli
index 5c936ff9d6..a138a457b3 100644
--- a/tactics/abstract.mli
+++ b/tactics/abstract.mli
@@ -20,3 +20,15 @@ val cache_term_by_tactic_then
-> unit Proofview.tactic
val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
+
+val declare_abstract :
+ ( name:Names.Id.t
+ -> poly:bool
+ -> kind:Decls.logical_kind
+ -> sign:EConstr.named_context
+ -> secsign:Environ.named_context_val
+ -> opaque:bool
+ -> solve_tac:unit Proofview.tactic
+ -> Evd.evar_map
+ -> EConstr.t
+ -> Evd.side_effects * Evd.evar_map * EConstr.t * EConstr.t list * bool) ref
diff --git a/tactics/declareUctx.ml b/tactics/declareUctx.ml
new file mode 100644
index 0000000000..3f67ff20a4
--- /dev/null
+++ b/tactics/declareUctx.ml
@@ -0,0 +1,34 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(* \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) *)
+(************************************************************************)
+
+(** Monomorphic universes need to survive sections. *)
+
+let name_instance inst =
+ let map lvl = match Univ.Level.name lvl with
+ | None -> (* Having Prop/Set/Var as section universes makes no sense *)
+ assert false
+ | Some na ->
+ try
+ let qid = Nametab.shortest_qualid_of_universe na in
+ Names.Name (Libnames.qualid_basename qid)
+ with Not_found ->
+ (* Best-effort naming from the string representation of the level.
+ See univNames.ml for a similar hack. *)
+ Names.Name (Names.Id.of_string_soft (Univ.Level.to_string lvl))
+ in
+ Array.map map (Univ.Instance.to_array inst)
+
+let declare_universe_context ~poly ctx =
+ if poly then
+ let uctx = Univ.ContextSet.to_context ctx in
+ let nas = name_instance (Univ.UContext.instance uctx) in
+ Global.push_section_context (nas, uctx)
+ else
+ Global.push_context_set ~strict:true ctx
diff --git a/tactics/declareUctx.mli b/tactics/declareUctx.mli
new file mode 100644
index 0000000000..7ecfab04f2
--- /dev/null
+++ b/tactics/declareUctx.mli
@@ -0,0 +1,11 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(* \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) *)
+(************************************************************************)
+
+val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 0499ba200e..5fb519cc4f 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -878,7 +878,7 @@ let fresh_global_or_constr env sigma poly cr =
else begin
if isgr then
warn_polymorphic_hint (pr_hint_term env sigma ctx cr);
- Declare.declare_universe_context ~poly:false ctx;
+ DeclareUctx.declare_universe_context ~poly:false ctx;
(c, Univ.ContextSet.empty)
end
@@ -1437,8 +1437,7 @@ let pr_hint_term env sigma cl =
(* print all hints that apply to the concl of the current goal *)
let pr_applicable_hint pf =
let env = Global.env () in
- let pts = Declare.Proof.get_proof pf in
- let Proof.{goals;sigma} = Proof.data pts in
+ let Proof.{goals;sigma} = Proof.data pf in
match goals with
| [] -> CErrors.user_err Pp.(str "No focused goal.")
| g::_ ->
diff --git a/tactics/hints.mli b/tactics/hints.mli
index a54da8ef0a..f5fd3348e4 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -288,7 +288,7 @@ val wrap_hint_warning_fun : env -> evar_map ->
(** Printing hints *)
val pr_searchtable : env -> evar_map -> Pp.t
-val pr_applicable_hint : Declare.Proof.t -> Pp.t
+val pr_applicable_hint : Proof.t -> Pp.t
val pr_hint_ref : env -> evar_map -> GlobRef.t -> Pp.t
val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t
val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 8336fae02f..e422366ed6 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -86,15 +86,15 @@ let compute_name internal id =
Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name
else id
+let declare_definition_scheme = ref (fun ~internal ~univs ~role ~name c ->
+ CErrors.anomaly (Pp.str "scheme declaration not registered"))
+
let define internal role id c poly univs =
let id = compute_name internal id in
let ctx = UState.minimize univs in
let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in
let univs = UState.univ_entry ~poly ctx in
- let entry = Declare.pure_definition_entry ~univs c in
- let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id entry in
- let () = if internal then () else Declare.definition_message id in
- kn, eff
+ !declare_definition_scheme ~internal ~univs ~role ~name:id c
let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
let (c, ctx), eff = f mode ind in
diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli
index dad2036c64..736de2af37 100644
--- a/tactics/ind_tables.mli
+++ b/tactics/ind_tables.mli
@@ -59,3 +59,11 @@ val check_scheme : 'a scheme_kind -> inductive -> bool
val lookup_scheme : 'a scheme_kind -> inductive -> Constant.t
val pr_scheme_kind : 'a scheme_kind -> Pp.t
+
+val declare_definition_scheme :
+ (internal : bool
+ -> univs:Entries.universes_entry
+ -> role:Evd.side_effect_role
+ -> name:Id.t
+ -> Constr.t
+ -> Constant.t * Evd.side_effects) ref
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 537d111f23..36d61feed1 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -1,5 +1,4 @@
DeclareScheme
-Declare
Dnet
Dn
Btermdn
@@ -18,7 +17,7 @@ Elim
Equality
Contradiction
Inv
-Leminv
+DeclareUctx
Hints
Auto
Eauto
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 43e86fa9bd..776ffd6b9f 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -91,7 +91,7 @@ let declare_assumptions ~poly ~scope ~kind univs nl l =
let () = match scope with
| Discharge ->
(* declare universes separately for variables *)
- Declare.declare_universe_context ~poly (context_set_of_entry (fst univs))
+ DeclareUctx.declare_universe_context ~poly (context_set_of_entry (fst univs))
| Global _ -> ()
in
let _, _ = List.fold_left (fun (subst,univs) ((is_coe,idl),typ,imps) ->
@@ -191,7 +191,7 @@ let context_subst subst (name,b,t,impl) =
let context_insection sigma ~poly ctx =
let uctx = Evd.universe_context_set sigma in
- let () = Declare.declare_universe_context ~poly uctx in
+ let () = DeclareUctx.declare_universe_context ~poly uctx in
let fn subst (name,_,_,_ as d) =
let d = context_subst subst d in
let () = match d with
@@ -226,7 +226,7 @@ let context_nosection sigma ~poly ctx =
(* Multiple monomorphic axioms: declare universes separately to
avoid redeclaring them. *)
let uctx = Evd.universe_context_set sigma in
- let () = Declare.declare_universe_context ~poly uctx in
+ let () = DeclareUctx.declare_universe_context ~poly uctx in
Monomorphic_entry Univ.ContextSet.empty
in
let fn subst d =
diff --git a/vernac/comHints.ml b/vernac/comHints.ml
index 324fee72ec..5a48e9c16c 100644
--- a/vernac/comHints.ml
+++ b/vernac/comHints.ml
@@ -97,7 +97,7 @@ let interp_hints ~poly h =
let c, diff = Hints.prepare_hint true env sigma (evd, c) in
if poly then (Hints.IsConstr (c, diff) [@ocaml.warning "-3"])
else
- let () = Declare.declare_universe_context ~poly:false diff in
+ let () = DeclareUctx.declare_universe_context ~poly:false diff in
(Hints.IsConstr (c, Univ.ContextSet.empty) [@ocaml.warning "-3"])
in
let fref r =
diff --git a/tactics/declare.ml b/vernac/declare.ml
index cce43e833e..6a4511ead8 100644
--- a/tactics/declare.ml
+++ b/vernac/declare.ml
@@ -133,31 +133,6 @@ let _ = CErrors.register_handler (function
type import_status = ImportDefaultBehavior | ImportNeedQualified
-(** Monomorphic universes need to survive sections. *)
-
-let name_instance inst =
- let map lvl = match Univ.Level.name lvl with
- | None -> (* Having Prop/Set/Var as section universes makes no sense *)
- assert false
- | Some na ->
- try
- let qid = Nametab.shortest_qualid_of_universe na in
- Name (Libnames.qualid_basename qid)
- with Not_found ->
- (* Best-effort naming from the string representation of the level.
- See univNames.ml for a similar hack. *)
- Name (Id.of_string_soft (Univ.Level.to_string lvl))
- in
- Array.map map (Univ.Instance.to_array inst)
-
-let declare_universe_context ~poly ctx =
- if poly then
- let uctx = Univ.ContextSet.to_context ctx in
- let nas = name_instance (Univ.UContext.instance uctx) in
- Global.push_section_context (nas, uctx)
- else
- Global.push_context_set ~strict:true ctx
-
(** Declaration of constants and parameters *)
type constant_obj = {
@@ -589,7 +564,7 @@ let declare_variable ~name ~kind d =
let univs = Univ.ContextSet.union body_ui entry_ui in
(* We must declare the universe constraints before type-checking the
term. *)
- let () = declare_universe_context ~poly univs in
+ let () = DeclareUctx.declare_universe_context ~poly univs in
let se = {
Entries.secdef_body = body;
secdef_secctx = de.proof_entry_secctx;
@@ -899,3 +874,13 @@ module Proof = struct
let update_global_env = update_global_env
let get_open_goals = get_open_goals
end
+
+let declare_definition_scheme ~internal ~univs ~role ~name c =
+ let kind = Decls.(IsDefinition Scheme) in
+ let entry = pure_definition_entry ~univs c in
+ let kn, eff = declare_private_constant ~role ~kind ~name entry in
+ let () = if internal then () else definition_message name in
+ kn, eff
+
+let _ = Ind_tables.declare_definition_scheme := declare_definition_scheme
+let _ = Abstract.declare_abstract := declare_abstract
diff --git a/tactics/declare.mli b/vernac/declare.mli
index 1fabf80b2a..73e0d7cd04 100644
--- a/tactics/declare.mli
+++ b/vernac/declare.mli
@@ -135,8 +135,6 @@ type 'a constant_entry =
| ParameterEntry of parameter_entry
| PrimitiveEntry of primitive_entry
-val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
-
val declare_variable
: name:variable
-> kind:Decls.logical_kind
@@ -262,19 +260,6 @@ val close_future_proof : feedback_id:Stateid.t -> Proof.t -> closed_proof_output
Returns [false] if an unsafe tactic has been used. *)
val by : unit Proofview.tactic -> Proof.t -> Proof.t * bool
-(** Declare abstract constant; will check no evars are possible; *)
-val declare_abstract :
- name:Names.Id.t
- -> poly:bool
- -> kind:Decls.logical_kind
- -> sign:EConstr.named_context
- -> secsign:Environ.named_context_val
- -> opaque:bool
- -> solve_tac:unit Proofview.tactic
- -> Evd.evar_map
- -> EConstr.t
- -> Evd.side_effects * Evd.evar_map * EConstr.t * EConstr.t list * bool
-
val build_by_tactic
: ?side_eff:bool
-> Environ.env
diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml
index 20fa43c8e7..89f3503f4d 100644
--- a/vernac/declareUniv.ml
+++ b/vernac/declareUniv.ml
@@ -94,7 +94,7 @@ let do_universe ~poly l =
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
+ DeclareUctx.declare_universe_context ~poly ctx
let do_constraint ~poly l =
let open Univ in
@@ -107,4 +107,4 @@ let do_constraint ~poly l =
Constraint.empty l
in
let uctx = ContextSet.add_constraints constraints ContextSet.empty in
- Declare.declare_universe_context ~poly uctx
+ DeclareUctx.declare_universe_context ~poly uctx
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 3d3be8050d..6d5d16d94a 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -9,6 +9,7 @@ Himsg
Locality
Egramml
Vernacextend
+Declare
ComHints
Ppvernac
Proof_using
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 028a7d0859..4958d0116e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1719,7 +1719,8 @@ let vernac_print ~pstate ~atts =
| PrintHintGoal ->
begin match pstate with
| Some pstate ->
- Hints.pr_applicable_hint pstate
+ let pf = Declare.Proof.get_proof pstate in
+ Hints.pr_applicable_hint pf
| None ->
str "No proof in progress"
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:45:01 +0000