aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrintern.ml27
-rw-r--r--interp/constrintern.mli11
-rw-r--r--plugins/funind/indfun.ml2
-rw-r--r--tactics/tacintern.ml12
-rw-r--r--tactics/tacinterp.ml20
5 files changed, 50 insertions, 22 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 04e9fceff..203d78bd2 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -66,6 +66,12 @@ type internalization_env =
type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr)
+type ltac_sign = {
+ ltac_vars : Id.Set.t;
+ ltac_bound : Id.Set.t;
+ ltac_subst : glob_constr Lazy.t Id.Map.t;
+}
+
let interning_grammar = ref false
(* Historically for parsing grammar rules, but in fact used only for
@@ -638,7 +644,6 @@ let string_of_ty = function
| Variable -> "var"
let intern_var genv (ltacvars,ntnvars) namedctx loc id =
- let (ltacvars,unbndltacvars,ltacsubst) = ltacvars in
(* Is [id] an inductive type potentially with implicit *)
try
let ty,expl_impls,impls,argsc = Id.Map.find id genv.impls in
@@ -649,12 +654,12 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
GVar (loc,id), make_implicits_list impls, argsc, expl_impls
with Not_found ->
(* Is [id] bound in current term or is an ltac var bound to constr *)
- if Id.Set.mem id genv.ids || Id.Set.mem id ltacvars
+ if Id.Set.mem id genv.ids || Id.Set.mem id ltacvars.ltac_vars
then
GVar (loc,id), [], [], []
(* Is [id] bound to a glob_constr in the the ltac context *)
- else if Id.Map.mem id ltacsubst then
- Lazy.force (Id.Map.find id ltacsubst), [], [], []
+ else if Id.Map.mem id ltacvars.ltac_subst then
+ Lazy.force (Id.Map.find id ltacvars.ltac_subst), [], [], []
(* Is [id] a notation variable *)
else if Id.Map.mem id ntnvars
then
@@ -664,7 +669,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
then if Id.Map.is_empty ntnvars
then error_ldots_var loc
else GVar (loc,id), [], [], []
- else if Id.Set.mem id unbndltacvars then
+ else if Id.Set.mem id ltacvars.ltac_bound then
(* Is [id] bound to a free name in ltac (this is an ltac error message) *)
user_err_loc (loc,"intern_var",
str "variable " ++ pr_id id ++ str " should be bound to a term.")
@@ -1549,9 +1554,9 @@ let internalize globalenv env allow_patvar lvar c =
let solve = match solve with
| None -> None
| Some gen ->
- let ((cvars, lvars,_), ntnvars) = lvar in
+ let (ltacvars, ntnvars) = lvar in
let ntnvars = Id.Map.domain ntnvars in
- let lvars = Id.Set.union lvars cvars 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 ist = {
@@ -1769,9 +1774,11 @@ let scope_of_type_kind = function
| OfType typ -> compute_type_scope typ
| WithoutTypeConstraint -> None
-type ltac_sign = Id.Set.t * Id.Set.t * glob_constr Lazy.t Id.Map.t
-
-let empty_ltac_sign = (Id.Set.empty, Id.Set.empty, Id.Map.empty)
+let empty_ltac_sign = {
+ ltac_vars = Id.Set.empty;
+ ltac_bound = Id.Set.empty;
+ ltac_subst = Id.Map.empty;
+}
let intern_gen kind env
?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=empty_ltac_sign)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 46697253b..b6cae349d 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -67,7 +67,16 @@ val compute_internalization_env : env -> var_internalization_type ->
Id.t list -> types list -> Impargs.manual_explicitation list list ->
internalization_env
-type ltac_sign = Id.Set.t * Id.Set.t * glob_constr Lazy.t Id.Map.t
+type ltac_sign = {
+ ltac_vars : Id.Set.t;
+ (** Variables of Ltac which may be bound to a term *)
+ ltac_bound : Id.Set.t;
+ (** Other variables of Ltac *)
+ ltac_subst : glob_constr Lazy.t Id.Map.t;
+ (** Substitution for untyped terms *)
+}
+
+val empty_ltac_sign : ltac_sign
type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 2ceda4f48..808b2604c 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -132,7 +132,7 @@ let rec abstract_glob_constr c = function
let interp_casted_constr_with_implicits sigma env impls c =
Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls
- ~allow_patvar:false ~ltacvars:(Id.Set.empty, Id.Set.empty,Id.Map.empty) c
+ ~allow_patvar:false c
(*
Construct a fixpoint as a Glob_term
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 2a66b32bc..c2f85d534 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -245,7 +245,11 @@ let intern_binding_name ist x =
let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env} 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 = (lfun, Id.Set.empty,Id.Map.empty) in
+ let ltacvars = {
+ Constrintern.ltac_vars = lfun;
+ ltac_bound = Id.Set.empty;
+ ltac_subst = Id.Map.empty;
+ } in
let c' =
warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars env) c
in
@@ -318,7 +322,11 @@ let intern_flag ist red =
let intern_constr_with_occurrences ist (l,c) = (l,intern_constr ist c)
let intern_constr_pattern ist ~as_type ~ltacvars pc =
- let ltacvars = ltacvars, Id.Set.empty,Id.Map.empty in
+ let ltacvars = {
+ Constrintern.ltac_vars = ltacvars;
+ ltac_bound = Id.Set.empty;
+ ltac_subst = Id.Map.empty;
+ } in
let metas,pat = Constrintern.intern_constr_pattern
ist.genv ~as_type ~ltacvars pc
in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 20234d1f2..cca26bf05 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -471,10 +471,12 @@ let extract_ltac_uconstr_values ist env =
let interp_uconstr ist env = function
| (c,None) -> c
| (_,Some ce) ->
- let ltacvars = extract_ltac_uconstr_values ist env in
- let bndvars = Id.Map.domain ist.lfun in
- let ltacdata = (Id.Set.empty, bndvars , ltacvars) in
- intern_gen WithoutTypeConstraint ~ltacvars:ltacdata env ce
+ let ltacvars = {
+ Constrintern.ltac_vars = Id.Set.empty;
+ ltac_bound = Id.Map.domain ist.lfun;
+ ltac_subst = extract_ltac_uconstr_values ist env;
+ } in
+ intern_gen WithoutTypeConstraint ~ltacvars env ce
let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
let constrvars = extract_ltac_constr_values ist env in
@@ -485,10 +487,12 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
context at globalization time: we retype with the now known
intros/lettac/inversion hypothesis names *)
| Some c ->
- let ltacvars = Id.Map.domain constrvars in
- let bndvars = Id.Map.domain ist.lfun in
- let ltacdata = (ltacvars, bndvars,Id.Map.empty) in
- intern_gen kind ~allow_patvar ~ltacvars:ltacdata env c
+ let ltacvars = {
+ ltac_vars = Id.Map.domain constrvars;
+ ltac_bound = Id.Map.domain ist.lfun;
+ ltac_subst = Id.Map.empty;
+ } in
+ intern_gen kind ~allow_patvar ~ltacvars env c
in
let trace =
push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-17 06:09:01 +0000