aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrintern.ml10
-rw-r--r--interp/constrintern.mli2
-rw-r--r--interp/genintern.ml12
-rw-r--r--interp/genintern.mli8
-rw-r--r--plugins/ltac/g_obligations.ml42
-rw-r--r--plugins/ltac/tacintern.ml24
-rw-r--r--plugins/ltac/tacintern.mli4
-rw-r--r--plugins/ltac/tacinterp.ml7
-rw-r--r--tactics/autorewrite.ml2
-rw-r--r--tactics/hints.ml2
-rw-r--r--vernac/vernacentries.ml2
11 files changed, 52 insertions, 23 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 3f99a3c7c..df7568c7a 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -68,6 +68,7 @@ type internalization_env =
type ltac_sign = {
ltac_vars : Id.Set.t;
ltac_bound : Id.Set.t;
+ ltac_extra : Genintern.Store.t;
}
let interning_grammar = ref false
@@ -1735,12 +1736,14 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
| Some gen ->
let (ltacvars, ntnvars) = lvar in
let ntnvars = Id.Map.domain ntnvars in
+ let extra = ltacvars.ltac_extra in
let lvars = Id.Set.union ltacvars.ltac_bound ltacvars.ltac_vars in
let lvars = Id.Set.union lvars ntnvars in
- let lvars = Id.Set.union lvars env.ids in
+ let ltacvars = Id.Set.union lvars env.ids in
let ist = {
- Genintern.ltacvars = lvars;
- genv = globalenv;
+ Genintern.genv = globalenv;
+ ltacvars;
+ extra;
} in
let (_, glb) = Genintern.generic_intern ist gen in
Some glb
@@ -1931,6 +1934,7 @@ let scope_of_type_kind = function
let empty_ltac_sign = {
ltac_vars = Id.Set.empty;
ltac_bound = Id.Set.empty;
+ ltac_extra = Genintern.Store.empty;
}
let intern_gen kind env
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index fdd50c6a1..644cafe57 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -70,6 +70,8 @@ type ltac_sign = {
(** Variables of Ltac which may be bound to a term *)
ltac_bound : Id.Set.t;
(** Other variables of Ltac *)
+ ltac_extra : Genintern.Store.t;
+ (** Arbitrary payload *)
}
val empty_ltac_sign : ltac_sign
diff --git a/interp/genintern.ml b/interp/genintern.ml
index be7abfa99..e443824bd 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -10,9 +10,19 @@ open Names
open Mod_subst
open Genarg
+module Store = Store.Make(struct end)
+
type glob_sign = {
ltacvars : Id.Set.t;
- genv : Environ.env }
+ genv : Environ.env;
+ extra : Store.t;
+}
+
+let empty_glob_sign env = {
+ ltacvars = Id.Set.empty;
+ genv = env;
+ extra = Store.empty;
+}
type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb
type 'glb subst_fun = substitution -> 'glb -> 'glb
diff --git a/interp/genintern.mli b/interp/genintern.mli
index 4b0354be3..658caa08c 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -10,9 +10,15 @@ open Names
open Mod_subst
open Genarg
+module Store : Store.S
+
type glob_sign = {
ltacvars : Id.Set.t;
- genv : Environ.env }
+ genv : Environ.env;
+ extra : Store.t;
+}
+
+val empty_glob_sign : Environ.env -> glob_sign
(** {5 Internalization functions} *)
diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index 3e6e2db60..a301daa57 100644
--- a/plugins/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
@@ -31,7 +31,7 @@ let () =
Obligations.default_tactic := tac
let with_tac f tac =
- let env = { Genintern.genv = Global.env (); ltacvars = Names.Id.Set.empty } in
+ let env = Genintern.empty_glob_sign (Global.env ()) in
let tac = match tac with
| None -> None
| Some tac ->
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 75227def0..40a299f76 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -41,13 +41,12 @@ let error_tactic_expected ?loc =
type glob_sign = Genintern.glob_sign = {
ltacvars : Id.Set.t;
(* ltac variables and the subset of vars introduced by Intro/Let/... *)
- genv : Environ.env }
+ genv : Environ.env;
+ extra : Genintern.Store.t;
+}
-let fully_empty_glob_sign =
- { ltacvars = Id.Set.empty; genv = Environ.empty_env }
-
-let make_empty_glob_sign () =
- { fully_empty_glob_sign with genv = Global.env () }
+let fully_empty_glob_sign = Genintern.empty_glob_sign Environ.empty_env
+let make_empty_glob_sign () = Genintern.empty_glob_sign (Global.env ())
(* We have identifier <| global_reference <| constr *)
@@ -192,12 +191,13 @@ let intern_binding_name ist x =
and if a term w/o ltac vars, check the name is indeed quantified *)
x
-let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env} c =
+let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env; extra} c =
let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in
let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in
let ltacvars = {
Constrintern.ltac_vars = lfun;
ltac_bound = Id.Set.empty;
+ ltac_extra = extra;
} in
let c' =
warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars env) c
@@ -313,6 +313,7 @@ let intern_constr_pattern ist ~as_type ~ltacvars pc =
let ltacvars = {
Constrintern.ltac_vars = ltacvars;
ltac_bound = Id.Set.empty;
+ ltac_extra = ist.extra;
} in
let metas,pat = Constrintern.intern_constr_pattern
ist.genv ~as_type ~ltacvars pc
@@ -344,7 +345,11 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
let r = match r with
| AN r -> r
| _ -> Qualid (loc,qualid_of_path (path_of_global (smart_global r))) in
- let sign = { Constrintern.ltac_vars = ist.ltacvars; Constrintern.ltac_bound = Id.Set.empty } in
+ let sign = {
+ Constrintern.ltac_vars = ist.ltacvars;
+ ltac_bound = Id.Set.empty;
+ ltac_extra = ist.extra;
+ } in
let c = Constrintern.interp_reference sign r in
match c with
| GRef (_,r,None) ->
@@ -708,8 +713,7 @@ let glob_tactic_env l env x =
let ltacvars =
List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in
Flags.with_option strict_check
- (intern_pure_tactic
- { ltacvars; genv = env })
+ (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars })
x
let split_ltac_fun = function
diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli
index 71ca354fa..8ad52ca02 100644
--- a/plugins/ltac/tacintern.mli
+++ b/plugins/ltac/tacintern.mli
@@ -18,7 +18,9 @@ open Misctypes
type glob_sign = Genintern.glob_sign = {
ltacvars : Id.Set.t;
- genv : Environ.env }
+ genv : Environ.env;
+ extra : Genintern.Store.t;
+}
val fully_empty_glob_sign : glob_sign
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index b8c021f18..5f831f326 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -587,6 +587,7 @@ let interp_uconstr ist env sigma = function
let ltacvars = {
Constrintern.ltac_vars = Id.(Set.union (Map.domain typed) (Map.domain untyped));
ltac_bound = Id.Map.domain ist.lfun;
+ ltac_extra = Genintern.Store.empty;
} in
{ closure ; term = intern_gen WithoutTypeConstraint ~ltacvars env ce }
@@ -614,6 +615,7 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
let ltacvars = {
ltac_vars = constr_context;
ltac_bound = Id.Map.domain ist.lfun;
+ ltac_extra = Genintern.Store.empty;
} in
let kind_for_intern =
match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in
@@ -1966,8 +1968,7 @@ let interp_tac_gen lfun avoid_ids debug t =
let ist = { lfun = lfun; extra = extra } in
let ltacvars = Id.Map.domain lfun in
interp_tactic ist
- (intern_pure_tactic {
- ltacvars; genv = env } t)
+ (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars } t)
end }
let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t
@@ -1976,7 +1977,7 @@ let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t
(* [global] means that [t] should be internalized outside of goals. *)
let hide_interp global t ot =
let hide_interp env =
- let ist = { ltacvars = Id.Set.empty; genv = env } in
+ let ist = Genintern.empty_glob_sign env in
let te = intern_pure_tactic ist t in
let t = eval_tactic te in
match ot with
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index e58ec5a31..900c8cc6f 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -305,7 +305,7 @@ let add_rew_rules base lrul =
let counter = ref 0 in
let env = Global.env () in
let sigma = Evd.from_env env in
- let ist = { Genintern.ltacvars = Id.Set.empty; genv = Global.env () } in
+ let ist = Genintern.empty_glob_sign (Global.env ()) in
let intern tac = snd (Genintern.generic_intern ist tac) in
let lrul =
List.fold_left
diff --git a/tactics/hints.ml b/tactics/hints.ml
index c5bacc5a2..aba04f30b 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1317,7 +1317,7 @@ let interp_hints poly =
let pat = Option.map fp patcom in
let l = match pat with None -> [] | Some (l, _) -> l in
let ltacvars = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in
- let env = Genintern.({ genv = env; ltacvars }) in
+ let env = Genintern.({ (empty_glob_sign env) with ltacvars }) in
let _, tacexp = Genintern.generic_intern env tacexp in
HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 2cb6f3918..e191ed0f2 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -844,7 +844,7 @@ let vernac_solve_existential = instantiate_nth_evar_com
let vernac_set_end_tac tac =
let open Genintern in
- let env = { genv = Global.env (); ltacvars = Id.Set.empty } in
+ let env = Genintern.empty_glob_sign (Global.env ()) in
let _, tac = Genintern.generic_intern env tac in
if not (refining ()) then
error "Unknown command of the non proof-editing mode.";
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 14:59:47 +0000