aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/evar_tactics.ml3
-rw-r--r--plugins/ltac/extratactics.ml430
-rw-r--r--plugins/ltac/taccoerce.ml3
-rw-r--r--plugins/ltac/taccoerce.mli11
-rw-r--r--plugins/ltac/tacexpr.mli2
-rw-r--r--plugins/ltac/tacintern.ml23
-rw-r--r--plugins/ltac/tacinterp.ml10
-rw-r--r--plugins/ltac/tacinterp.mli8
-rw-r--r--plugins/ltac/tactic_debug.ml2
-rw-r--r--plugins/ltac/tactic_matching.ml6
-rw-r--r--plugins/ltac/tactic_matching.mli2
11 files changed, 57 insertions, 43 deletions
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index d9150a7bbd..1f628803a3 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -17,6 +17,7 @@ open Refiner
open Evd
open Locus
open Context.Named.Declaration
+open Ltac_pretype
module NamedDecl = Context.Named.Declaration
@@ -27,7 +28,7 @@ let instantiate_evar evk (ist,rawc) sigma =
let filtered = Evd.evar_filtered_env evi in
let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in
let lvar = {
- Glob_term.ltac_constrs = constrvars;
+ ltac_constrs = constrvars;
ltac_uconstrs = Names.Id.Map.empty;
ltac_idents = Names.Id.Map.empty;
ltac_genargs = ist.Geninterp.lfun;
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index a7aebf9e15..65c186a419 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -91,12 +91,12 @@ let elimOnConstrWithHoles tac with_evars c =
(fun c -> tac with_evars (Some (None,ElimOnConstr c)))
TACTIC EXTEND simplify_eq
- [ "simplify_eq" ] -> [ dEq false None ]
-| [ "simplify_eq" destruction_arg(c) ] -> [ mytclWithHoles dEq false c ]
+ [ "simplify_eq" ] -> [ dEq ~keep_proofs:None false None ]
+| [ "simplify_eq" destruction_arg(c) ] -> [ mytclWithHoles (dEq ~keep_proofs:None) false c ]
END
TACTIC EXTEND esimplify_eq
-| [ "esimplify_eq" ] -> [ dEq true None ]
-| [ "esimplify_eq" destruction_arg(c) ] -> [ mytclWithHoles dEq true c ]
+| [ "esimplify_eq" ] -> [ dEq ~keep_proofs:None true None ]
+| [ "esimplify_eq" destruction_arg(c) ] -> [ mytclWithHoles (dEq ~keep_proofs:None) true c ]
END
let discr_main c = elimOnConstrWithHoles discr_tac false c
@@ -117,31 +117,31 @@ let discrHyp id =
discr_main (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings)))
let injection_main with_evars c =
- elimOnConstrWithHoles (injClause None) with_evars c
+ elimOnConstrWithHoles (injClause None None) with_evars c
TACTIC EXTEND injection
-| [ "injection" ] -> [ injClause None false None ]
-| [ "injection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None) false c ]
+| [ "injection" ] -> [ injClause None None false None ]
+| [ "injection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None None) false c ]
END
TACTIC EXTEND einjection
-| [ "einjection" ] -> [ injClause None true None ]
-| [ "einjection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None) true c ]
+| [ "einjection" ] -> [ injClause None None true None ]
+| [ "einjection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None None) true c ]
END
TACTIC EXTEND injection_as
| [ "injection" "as" intropattern_list(ipat)] ->
- [ injClause (Some ipat) false None ]
+ [ injClause None (Some ipat) false None ]
| [ "injection" destruction_arg(c) "as" intropattern_list(ipat)] ->
- [ mytclWithHoles (injClause (Some ipat)) false c ]
+ [ mytclWithHoles (injClause None (Some ipat)) false c ]
END
TACTIC EXTEND einjection_as
| [ "einjection" "as" intropattern_list(ipat)] ->
- [ injClause (Some ipat) true None ]
+ [ injClause None (Some ipat) true None ]
| [ "einjection" destruction_arg(c) "as" intropattern_list(ipat)] ->
- [ mytclWithHoles (injClause (Some ipat)) true c ]
+ [ mytclWithHoles (injClause None (Some ipat)) true c ]
END
TACTIC EXTEND simple_injection
-| [ "simple" "injection" ] -> [ simpleInjClause false None ]
-| [ "simple" "injection" destruction_arg(c) ] -> [ mytclWithHoles simpleInjClause false c ]
+| [ "simple" "injection" ] -> [ simpleInjClause None false None ]
+| [ "simple" "injection" destruction_arg(c) ] -> [ mytclWithHoles (simpleInjClause None) false c ]
END
let injHyp id =
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 9e3a54cc86..a79a92a661 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -10,7 +10,6 @@ open Util
open Names
open Term
open EConstr
-open Pattern
open Misctypes
open Genarg
open Stdarg
@@ -24,7 +23,7 @@ let (wit_constr_context : (Empty.t, Empty.t, EConstr.constr) Genarg.genarg_type)
wit
(* includes idents known to be bound and references *)
-let (wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) Genarg.genarg_type) =
+let (wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_binders) Genarg.genarg_type) =
let wit = Genarg.create_arg "constr_under_binders" in
let () = register_val0 wit None in
wit
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 1a67f6f888..d7b253a687 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -10,7 +10,6 @@ open Util
open Names
open EConstr
open Misctypes
-open Pattern
open Genarg
open Geninterp
@@ -37,8 +36,8 @@ sig
val of_constr : constr -> t
val to_constr : t -> constr option
- val of_uconstr : Glob_term.closed_glob_constr -> t
- val to_uconstr : t -> Glob_term.closed_glob_constr option
+ val of_uconstr : Ltac_pretype.closed_glob_constr -> t
+ val to_uconstr : t -> Ltac_pretype.closed_glob_constr option
val of_int : int -> t
val to_int : t -> int option
val to_list : t -> t list option
@@ -63,9 +62,9 @@ val coerce_to_hint_base : Value.t -> string
val coerce_to_int : Value.t -> int
-val coerce_to_constr : Environ.env -> Value.t -> constr_under_binders
+val coerce_to_constr : Environ.env -> Value.t -> Ltac_pretype.constr_under_binders
-val coerce_to_uconstr : Environ.env -> Value.t -> Glob_term.closed_glob_constr
+val coerce_to_uconstr : Environ.env -> Value.t -> Ltac_pretype.closed_glob_constr
val coerce_to_closed_constr : Environ.env -> Value.t -> constr
@@ -93,4 +92,4 @@ val coerce_to_int_or_var_list : Value.t -> int or_var list
val wit_constr_context : (Empty.t, Empty.t, EConstr.constr) genarg_type
-val wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) genarg_type
+val wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_binders) genarg_type
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 2c36faeff4..1639736883 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -386,7 +386,7 @@ type ltac_call_kind =
| LtacNameCall of ltac_constant
| LtacAtomCall of glob_atomic_tactic_expr
| LtacVarCall of Id.t * glob_tactic_expr
- | LtacConstrInterp of Glob_term.glob_constr * Glob_term.ltac_var_map
+ | LtacConstrInterp of Glob_term.glob_constr * Ltac_pretype.ltac_var_map
type ltac_trace = ltac_call_kind Loc.located list
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 99d7684d36..f171fd07d7 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -322,13 +322,23 @@ let intern_constr_pattern ist ~as_type ~ltacvars pc =
let dummy_pat = PRel 0
-let intern_typed_pattern ist p =
+let intern_typed_pattern ist ~as_type ~ltacvars p =
(* we cannot ensure in non strict mode that the pattern is closed *)
(* keeping a constr_expr copy is too complicated and we want anyway to *)
(* type it, so we remember the pattern as a glob_constr only *)
+ let metas,pat =
+ if !strict_check then
+ let ltacvars = {
+ Constrintern.ltac_vars = ltacvars;
+ ltac_bound = Id.Set.empty;
+ ltac_extra = ist.extra;
+ } in
+ Constrintern.intern_constr_pattern ist.genv ~as_type ~ltacvars p
+ else
+ [], dummy_pat in
let (glob,_ as c) = intern_constr_gen true false ist p in
let bound_names = Glob_ops.bound_glob_vars glob in
- (bound_names,c,dummy_pat)
+ metas,(bound_names,c,pat)
let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
let interp_ref r =
@@ -364,7 +374,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
(* We interpret similarly @ref and ref *)
interp_ref (AN r)
| Inr c ->
- Inr (intern_typed_pattern ist c))
+ Inr (snd (intern_typed_pattern ist ~as_type:false ~ltacvars:ist.ltacvars c)))
(* This seems fairly hacky, but it's the first way I've found to get proper
globalization of [unfold]. --adamc *)
@@ -529,7 +539,12 @@ let rec intern_atomic lf ist x =
then intern_type ist c else intern_constr ist c),
clause_app (intern_hyp_location ist) cl)
| TacChange (Some p,c,cl) ->
- TacChange (Some (intern_typed_pattern ist p),intern_constr ist c,
+ let { ltacvars } = ist in
+ let metas,pat = intern_typed_pattern ist ~as_type:false ~ltacvars p in
+ let fold accu x = Id.Set.add x accu in
+ let ltacvars = List.fold_left fold ltacvars metas in
+ let ist' = { ist with ltacvars } in
+ TacChange (Some pat,intern_constr ist' c,
clause_app (intern_hyp_location ist) cl)
(* Equality and inversion *)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 20f117ff4f..66f124d2d1 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -38,6 +38,7 @@ open Tacintern
open Taccoerce
open Proofview.Notations
open Context.Named.Declaration
+open Ltac_pretype
let ltac_trace_info = Tactic_debug.ltac_trace_info
@@ -551,7 +552,6 @@ let interp_fresh_id ist env sigma l =
(* Extract the uconstr list from lfun *)
let extract_ltac_constr_context ist env sigma =
- let open Glob_term in
let add_uconstr id v map =
try Id.Map.add id (coerce_to_uconstr env v) map
with CannotCoerceTo _ -> map
@@ -602,10 +602,10 @@ let interp_gen kind ist pattern_mode flags env sigma c =
let { closure = constrvars ; term } =
interp_glob_closure ist env sigma ~kind:kind_for_intern ~pattern_mode c in
let vars = {
- Glob_term.ltac_constrs = constrvars.typed;
- Glob_term.ltac_uconstrs = constrvars.untyped;
- Glob_term.ltac_idents = constrvars.idents;
- Glob_term.ltac_genargs = ist.lfun;
+ ltac_constrs = constrvars.typed;
+ ltac_uconstrs = constrvars.untyped;
+ ltac_idents = constrvars.idents;
+ ltac_genargs = ist.lfun;
} in
(* Jason Gross: To avoid unnecessary modifications to tacinterp, as
suggested by Arnaud Spiwack, we run push_trace immediately. We do
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index d0a0a81d4c..5f2723a1e3 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -44,7 +44,7 @@ val f_avoid_ids : Id.Set.t TacStore.field
val f_debug : debug_info TacStore.field
val extract_ltac_constr_values : interp_sign -> Environ.env ->
- Pattern.constr_under_binders Id.Map.t
+ Ltac_pretype.constr_under_binders Id.Map.t
(** Given an interpretation signature, extract all values which are coercible to
a [constr]. *)
@@ -57,7 +57,7 @@ val get_debug : unit -> debug_info
val type_uconstr :
?flags:Pretyping.inference_flags ->
?expected_type:Pretyping.typing_constraint ->
- Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr Tactypes.delayed_open
+ Geninterp.interp_sign -> Ltac_pretype.closed_glob_constr -> constr Tactypes.delayed_open
(** Adds an interpretation function for extra generic arguments *)
@@ -79,10 +79,10 @@ val interp_hyp : interp_sign -> Environ.env -> Evd.evar_map ->
val interp_glob_closure : interp_sign -> Environ.env -> Evd.evar_map ->
?kind:Pretyping.typing_constraint -> ?pattern_mode:bool -> glob_constr_and_expr ->
- Glob_term.closed_glob_constr
+ Ltac_pretype.closed_glob_constr
val interp_uconstr : interp_sign -> Environ.env -> Evd.evar_map ->
- glob_constr_and_expr -> Glob_term.closed_glob_constr
+ glob_constr_and_expr -> Ltac_pretype.closed_glob_constr
val interp_constr_gen : Pretyping.typing_constraint -> interp_sign ->
Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Evd.evar_map * constr
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 5394b1e116..a669692fc9 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -363,7 +363,7 @@ let explain_ltac_call_trace last trace loc =
| Tacexpr.LtacAtomCall te ->
quote (Pptactic.pr_glob_tactic (Global.env())
(Tacexpr.TacAtom (Loc.tag te)))
- | Tacexpr.LtacConstrInterp (c, { Glob_term.ltac_constrs = vars }) ->
+ | Tacexpr.LtacConstrInterp (c, { Ltac_pretype.ltac_constrs = vars }) ->
quote (Printer.pr_glob_constr_env (Global.env()) c) ++
(if not (Id.Map.is_empty vars) then
strbrk " (with " ++
diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml
index 18bb7d2dbd..89b78e5907 100644
--- a/plugins/ltac/tactic_matching.ml
+++ b/plugins/ltac/tactic_matching.ml
@@ -22,7 +22,7 @@ module NamedDecl = Context.Named.Declaration
those of {!Matching.matching_result}), and a {!Term.constr}
substitution mapping corresponding to matched hypotheses. *)
type 'a t = {
- subst : Constr_matching.bound_ident_map * Pattern.extended_patvar_map ;
+ subst : Constr_matching.bound_ident_map * Ltac_pretype.extended_patvar_map ;
context : EConstr.constr Id.Map.t;
terms : EConstr.constr Id.Map.t;
lhs : 'a;
@@ -36,8 +36,8 @@ type 'a t = {
(** Some of the functions of {!Matching} return the substitution with a
[patvar_map] instead of an [extended_patvar_map]. [adjust] coerces
substitution of the former type to the latter. *)
-let adjust : Constr_matching.bound_ident_map * Pattern.patvar_map ->
- Constr_matching.bound_ident_map * Pattern.extended_patvar_map =
+let adjust : Constr_matching.bound_ident_map * Ltac_pretype.patvar_map ->
+ Constr_matching.bound_ident_map * Ltac_pretype.extended_patvar_map =
fun (l, lc) -> (l, Id.Map.map (fun c -> [], c) lc)
diff --git a/plugins/ltac/tactic_matching.mli b/plugins/ltac/tactic_matching.mli
index 01334d36c9..955f8105fb 100644
--- a/plugins/ltac/tactic_matching.mli
+++ b/plugins/ltac/tactic_matching.mli
@@ -18,7 +18,7 @@
those of {!Matching.matching_result}), and a {!Term.constr}
substitution mapping corresponding to matched hypotheses. *)
type 'a t = {
- subst : Constr_matching.bound_ident_map * Pattern.extended_patvar_map ;
+ subst : Constr_matching.bound_ident_map * Ltac_pretype.extended_patvar_map ;
context : EConstr.constr Names.Id.Map.t;
terms : EConstr.constr Names.Id.Map.t;
lhs : 'a;
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 11:41:07 +0000