aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--tactics/declare.ml5
-rw-r--r--tactics/declare.mli5
-rw-r--r--tactics/declareScheme.ml42
-rw-r--r--tactics/declareScheme.mli12
-rw-r--r--tactics/ind_tables.ml38
-rw-r--r--tactics/ind_tables.mli4
-rw-r--r--tactics/tactics.mllib1
7 files changed, 62 insertions, 45 deletions
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 9f104590e7..fb06bb8a4f 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -139,9 +139,6 @@ let (inConstant : constant_obj -> obj) =
subst_function = ident_subst_function;
discharge_function = discharge_constant }
-let declare_scheme = ref (fun _ _ -> assert false)
-let set_declare_scheme f = declare_scheme := f
-
let update_tables c =
Impargs.declare_constant_implicits c;
Notation.declare_ref_arguments_scope Evd.empty (GlobRef.ConstRef c)
@@ -159,7 +156,7 @@ let register_side_effect (c, role) =
let () = register_constant c Decls.(IsProof Theorem) ImportDefaultBehavior in
match role with
| None -> ()
- | Some (Evd.Schema (ind, kind)) -> !declare_scheme kind [|ind,c|]
+ | Some (Evd.Schema (ind, kind)) -> DeclareScheme.declare_scheme kind [|ind,c|]
let record_aux env s_ty s_bo =
let open Environ in
diff --git a/tactics/declare.mli b/tactics/declare.mli
index a4d3f17594..c646d2f85b 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -117,11 +117,6 @@ val inline_private_constants
-> Evd.side_effects proof_entry
-> Constr.t * UState.t
-(** Since transparent constants' side effects are globally declared, we
- * need that *)
-val set_declare_scheme :
- (string -> (inductive * Constant.t) array -> unit) -> unit
-
(** Declaration messages *)
val definition_message : Id.t -> unit
diff --git a/tactics/declareScheme.ml b/tactics/declareScheme.ml
new file mode 100644
index 0000000000..5f4626fcb2
--- /dev/null
+++ b/tactics/declareScheme.ml
@@ -0,0 +1,42 @@
+(************************************************************************)
+(* * 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
+
+let scheme_map = Summary.ref Indmap.empty ~name:"Schemes"
+
+let cache_one_scheme kind (ind,const) =
+ let map = try Indmap.find ind !scheme_map with Not_found -> CString.Map.empty in
+ scheme_map := Indmap.add ind (CString.Map.add kind const map) !scheme_map
+
+let cache_scheme (_,(kind,l)) =
+ Array.iter (cache_one_scheme kind) l
+
+let subst_one_scheme subst (ind,const) =
+ (* Remark: const is a def: the result of substitution is a constant *)
+ (Mod_subst.subst_ind subst ind, Mod_subst.subst_constant subst const)
+
+let subst_scheme (subst,(kind,l)) =
+ (kind, CArray.Smart.map (subst_one_scheme subst) l)
+
+let discharge_scheme (_,(kind,l)) =
+ Some (kind, l)
+
+let inScheme : string * (inductive * Constant.t) array -> Libobject.obj =
+ let open Libobject in
+ declare_object @@ superglobal_object "SCHEME"
+ ~cache:cache_scheme
+ ~subst:(Some subst_scheme)
+ ~discharge:discharge_scheme
+
+let declare_scheme kind indcl =
+ Lib.add_anonymous_leaf (inScheme (kind,indcl))
+
+let lookup_scheme kind ind = CString.Map.find kind (Indmap.find ind !scheme_map)
diff --git a/tactics/declareScheme.mli b/tactics/declareScheme.mli
new file mode 100644
index 0000000000..f2ae5e41c8
--- /dev/null
+++ b/tactics/declareScheme.mli
@@ -0,0 +1,12 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+val declare_scheme : string -> (Names.inductive * Names.Constant.t) array -> unit
+val lookup_scheme : string -> Names.inductive -> Names.Constant.t
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index ac98b5f116..9c94f3c319 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -15,8 +15,6 @@
declaring schemes and generating schemes on demand *)
open Names
-open Mod_subst
-open Libobject
open Nameops
open Declarations
open Constr
@@ -40,33 +38,8 @@ type individual_scheme_object_function =
type 'a scheme_kind = string
-let scheme_map = Summary.ref Indmap.empty ~name:"Schemes"
-
let pr_scheme_kind = Pp.str
-let cache_one_scheme kind (ind,const) =
- let map = try Indmap.find ind !scheme_map with Not_found -> String.Map.empty in
- scheme_map := Indmap.add ind (String.Map.add kind const map) !scheme_map
-
-let cache_scheme (_,(kind,l)) =
- Array.iter (cache_one_scheme kind) l
-
-let subst_one_scheme subst (ind,const) =
- (* Remark: const is a def: the result of substitution is a constant *)
- (subst_ind subst ind,subst_constant subst const)
-
-let subst_scheme (subst,(kind,l)) =
- (kind,Array.Smart.map (subst_one_scheme subst) l)
-
-let discharge_scheme (_,(kind,l)) =
- Some (kind, l)
-
-let inScheme : string * (inductive * Constant.t) array -> obj =
- declare_object @@ superglobal_object "SCHEME"
- ~cache:cache_scheme
- ~subst:(Some subst_scheme)
- ~discharge:discharge_scheme
-
(**********************************************************************)
(* The table of scheme building functions *)
@@ -104,11 +77,6 @@ let declare_individual_scheme_object s ?(aux="") f =
(**********************************************************************)
(* Defining/retrieving schemes *)
-let declare_scheme kind indcl =
- Lib.add_anonymous_leaf (inScheme (kind,indcl))
-
-let () = Declare.set_declare_scheme declare_scheme
-
let is_visible_name id =
try ignore (Nametab.locate (Libnames.qualid_of_ident id)); true
with Not_found -> false
@@ -140,7 +108,7 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
| None -> add_suffix mib.mind_packets.(i).mind_typename suff in
let role = Evd.Schema (ind, kind) in
let const, neff = define mode role id c (Declareops.inductive_is_polymorphic mib) ctx in
- declare_scheme kind [|ind,const|];
+ DeclareScheme.declare_scheme kind [|ind,const|];
const, Evd.concat_side_effects neff eff
let define_individual_scheme kind mode names (mind,i as ind) =
@@ -162,7 +130,7 @@ let define_mutual_scheme_base kind suff f mode names mind =
in
let (eff, consts) = Array.fold_left2_map_i fold eff ids cl in
let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in
- declare_scheme kind schemes;
+ DeclareScheme.declare_scheme kind schemes;
consts, eff
let define_mutual_scheme kind mode names mind =
@@ -172,7 +140,7 @@ let define_mutual_scheme kind mode names mind =
define_mutual_scheme_base kind s f mode names mind
let find_scheme_on_env_too kind ind =
- let s = String.Map.find kind (Indmap.find ind !scheme_map) in
+ let s = DeclareScheme.lookup_scheme kind ind in
s, Evd.empty_side_effects
let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) =
diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli
index 17e9c7ef42..e9a792c264 100644
--- a/tactics/ind_tables.mli
+++ b/tactics/ind_tables.mli
@@ -30,7 +30,9 @@ type mutual_scheme_object_function =
type individual_scheme_object_function =
internal_flag -> inductive -> constr Evd.in_evar_universe_context * Evd.side_effects
-(** Main functions to register a scheme builder *)
+(** Main functions to register a scheme builder. Note these functions
+ are not safe to be used by plugins as their effects won't be undone
+ on backtracking *)
val declare_mutual_scheme_object : string -> ?aux:string ->
mutual_scheme_object_function -> mutual scheme_kind
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index c5c7969a09..0c4e496650 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -1,3 +1,4 @@
+DeclareScheme
Declare
Proof_global
Pfedit
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:13:10 +0000