aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrarg.ml2
-rw-r--r--interp/constrarg.mli3
-rw-r--r--intf/tacexpr.mli13
-rw-r--r--plugins/funind/g_indfun.ml45
-rw-r--r--plugins/funind/indfun.mli2
-rw-r--r--printing/pptactic.ml2
-rw-r--r--tactics/equality.mli3
-rw-r--r--tactics/inv.mli6
-rw-r--r--tactics/taccoerce.mli2
-rw-r--r--tactics/tacinterp.ml6
-rw-r--r--tactics/tacticals.ml2
-rw-r--r--tactics/tacticals.mli14
-rw-r--r--tactics/tactics.ml21
-rw-r--r--tactics/tactics.mli16
14 files changed, 54 insertions, 43 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 9c1382ba1..67282e5dd 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -24,7 +24,7 @@ let unsafe_of_type (t : argument_type) : ('a, 'b, 'c) Genarg.genarg_type =
let wit_int_or_var = unsafe_of_type IntOrVarArgType
-let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, constr intro_pattern_expr located) genarg_type =
+let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type =
Genarg.make0 None "intropattern"
let wit_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type =
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index b6ff3c850..ab3d7eafd 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -28,8 +28,7 @@ val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t
val wit_int_or_var : int or_var uniform_genarg_type
-val wit_intro_pattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, constr intro_pattern_expr located) genarg_type
-
+val wit_intro_pattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type
val wit_ident : Id.t uniform_genarg_type
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 9b75282ca..abb2292cd 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -106,9 +106,16 @@ type open_glob_constr = unit * glob_constr_and_expr
type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern
-type intro_pattern = Term.constr intro_pattern_expr located
-type intro_patterns = Term.constr intro_pattern_expr located list
-type or_and_intro_pattern = Term.constr or_and_intro_pattern_expr located
+type delayed_open_constr_with_bindings =
+ Environ.env -> Evd.evar_map -> Evd.evar_map * Term.constr with_bindings
+
+type delayed_open_constr =
+ Environ.env -> Evd.evar_map -> Evd.evar_map * Term.constr
+
+type intro_pattern = delayed_open_constr intro_pattern_expr located
+type intro_patterns = delayed_open_constr intro_pattern_expr located list
+type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr located
+type intro_pattern_naming = intro_pattern_naming_expr located
(** Generic expressions for atomic tactics *)
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index e688204a4..bbb8a96c5 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -78,10 +78,13 @@ END
let pr_intro_as_pat prc _ _ pat =
+ failwith "todo"
+(*
match pat with
| Some pat ->
- spc () ++ str "as" ++ spc () ++ Miscprint.pr_intro_pattern prc pat
+ spc () ++ str "as" ++ spc () ++ Miscprint.pr_intro_pattern prc pat
| None -> mt ()
+*)
let out_disjunctive = function
| loc, IntroAction (IntroOrAndPattern l) -> (loc,l)
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index 34985f2c4..e72069140 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -10,7 +10,7 @@ val functional_induction :
bool ->
Term.constr ->
(Term.constr * Term.constr bindings) option ->
- Term.constr or_and_intro_pattern_expr Loc.located option ->
+ Tacexpr.or_and_intro_pattern option ->
Proof_type.goal Tacmach.sigma -> Proof_type.goal list Evd.sigma
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 5ea4293c9..8c3e9a7e0 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1024,7 +1024,7 @@ let () =
Constrarg.wit_intro_pattern
(Miscprint.pr_intro_pattern pr_constr_expr)
(Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c))
- (Miscprint.pr_intro_pattern pr_constr);
+ (Miscprint.pr_intro_pattern (fun c -> pr_constr (snd (c (Global.env()) Evd.empty))));
Genprint.register_print0
Constrarg.wit_clause_dft_concl
(pr_clauses (Some true) pr_lident)
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 9008af77b..5ac4fccb8 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -60,9 +60,6 @@ val general_rewrite_in :
val general_rewrite_clause :
orientation -> evars_flag -> ?tac:(unit Proofview.tactic * conditions) -> constr with_bindings -> clause -> unit Proofview.tactic
-type delayed_open_constr_with_bindings =
- env -> evar_map -> evar_map * constr with_bindings
-
val general_multi_rewrite :
evars_flag -> (bool * multi * clear_flag * delayed_open_constr_with_bindings) list ->
clause -> (unit Proofview.tactic * conditions) option -> unit Proofview.tactic
diff --git a/tactics/inv.mli b/tactics/inv.mli
index a71b5eeb3..c730716d8 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -15,14 +15,14 @@ open Tacexpr
type inversion_status = Dep of constr option | NoDep
val inv_clause :
- inversion_kind -> constr or_and_intro_pattern_expr located option -> Id.t list ->
+ inversion_kind -> or_and_intro_pattern option -> Id.t list ->
quantified_hypothesis -> unit Proofview.tactic
-val inv : inversion_kind -> constr or_and_intro_pattern_expr located option ->
+val inv : inversion_kind -> or_and_intro_pattern option ->
quantified_hypothesis -> unit Proofview.tactic
val dinv : inversion_kind -> constr option ->
- constr or_and_intro_pattern_expr located option -> quantified_hypothesis -> unit Proofview.tactic
+ or_and_intro_pattern option -> quantified_hypothesis -> unit Proofview.tactic
val inv_tac : Id.t -> unit Proofview.tactic
val inv_clear_tac : Id.t -> unit Proofview.tactic
diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli
index 629a218e5..cec25d9bd 100644
--- a/tactics/taccoerce.mli
+++ b/tactics/taccoerce.mli
@@ -50,7 +50,7 @@ val coerce_to_constr_context : Value.t -> constr
val coerce_to_ident : bool -> Environ.env -> Value.t -> Id.t
-val coerce_to_intro_pattern : Environ.env -> Value.t -> constr intro_pattern_expr
+val coerce_to_intro_pattern : Environ.env -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr
val coerce_to_intro_pattern_naming :
Environ.env -> Value.t -> intro_pattern_naming_expr
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 026ed94a4..df3115265 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -725,7 +725,9 @@ let rec message_of_value env v =
else if has_type v (topwit wit_unit) then str "()"
else if has_type v (topwit wit_int) then int (out_gen (topwit wit_int) v)
else if has_type v (topwit wit_intro_pattern) then
- Miscprint.pr_intro_pattern (pr_constr_env env) (out_gen (topwit wit_intro_pattern) v)
+ Miscprint.pr_intro_pattern
+ (fun c -> pr_constr_env env (snd (c env Evd.empty)))
+ (out_gen (topwit wit_intro_pattern) v)
else if has_type v (topwit wit_constr_context) then
pr_constr_env env (out_gen (topwit wit_constr_context) v)
else match Value.to_list v with
@@ -776,7 +778,7 @@ and interp_intro_pattern_action ist env sigma = function
let sigma,l = interp_intro_pattern_list_as_list ist env sigma l in
sigma, IntroInjection l
| IntroApplyOn (c,ipat) ->
- let sigma,c = interp_constr ist env sigma c in
+ let c = fun env sigma -> interp_constr ist env sigma c in
let sigma,ipat = interp_intro_pattern ist env sigma ipat in
sigma, IntroApplyOn (c,ipat)
| IntroRewrite _ as x -> sigma, x
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 840cd0c05..bbd114c28 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -151,7 +151,7 @@ type branch_args = {
nassums : int; (* the number of assumptions to be introduced *)
branchsign : bool list; (* the signature of the branch.
true=recursive argument, false=constant *)
- branchnames : constr intro_pattern_expr Loc.located list}
+ branchnames : Tacexpr.intro_patterns}
type branch_assumptions = {
ba : branch_args; (* the branch args *)
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index de2bbbfae..54aa3b697 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -117,16 +117,16 @@ type branch_assumptions = {
(** [check_disjunctive_pattern_size loc pats n] returns an appropriate
error message if |pats| <> n *)
val check_or_and_pattern_size :
- Loc.t -> constr or_and_intro_pattern_expr -> int -> unit
+ Loc.t -> delayed_open_constr or_and_intro_pattern_expr -> int -> unit
(** Tolerate "[]" to mean a disjunctive pattern of any length *)
-val fix_empty_or_and_pattern : int -> constr or_and_intro_pattern_expr ->
- constr or_and_intro_pattern_expr
+val fix_empty_or_and_pattern : int ->
+ delayed_open_constr or_and_intro_pattern_expr ->
+ delayed_open_constr or_and_intro_pattern_expr
(** Useful for [as intro_pattern] modifier *)
val compute_induction_names :
- int -> constr or_and_intro_pattern_expr located option ->
- intro_patterns array
+ int -> or_and_intro_pattern option -> intro_patterns array
val elimination_sort_of_goal : goal sigma -> sorts_family
val elimination_sort_of_hyp : Id.t -> goal sigma -> sorts_family
@@ -242,11 +242,11 @@ module New : sig
constr -> unit Proofview.tactic
val case_then_using :
- constr or_and_intro_pattern_expr located option -> (branch_args -> unit Proofview.tactic) ->
+ or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) ->
constr option -> pinductive -> Term.constr * Term.types -> unit Proofview.tactic
val case_nodep_then_using :
- constr or_and_intro_pattern_expr located option -> (branch_args -> unit Proofview.tactic) ->
+ or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) ->
constr option -> pinductive -> Term.constr * Term.types -> unit Proofview.tactic
val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 44043364d..62c3a8fc1 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1805,14 +1805,21 @@ and intro_pattern_action loc b style pat thin tac id = match pat with
(* Skip the side conditions of the rewriting step *)
(rewrite_hyp style l2r id)
(tac thin None [])
- | IntroApplyOn (c,(loc,pat)) ->
+ | IntroApplyOn (f,(loc,pat)) ->
let naming,tac_ipat = prepare_intros_loc loc (IntroIdentifier id) pat in
let clear = do_replace (Some id) naming in
- Tacticals.New.tclTHENFIRST
- (* Skip the side conditions of the apply *)
- (apply_in_once false true true true (Some (clear,naming)) id
- (None,(Evd.empty,(c,NoBindings))) tac_ipat)
- (tac thin None [])
+ Proofview.Goal.raw_enter begin fun gl ->
+ let sigma = Proofview.Goal.sigma gl in
+ let env = Proofview.Goal.env gl in
+ let sigma,c = f env sigma in
+ Tacticals.New.tclWITHHOLES false
+ (Tacticals.New.tclTHENFIRST
+ (* Skip the side conditions of the apply *)
+ (apply_in_once false true true true (Some (clear,naming)) id
+ (None,(sigma,(c,NoBindings))) tac_ipat))
+ sigma
+ (tac thin None [])
+ end
and prepare_intros_loc loc dft = function
| IntroNaming ipat ->
@@ -2228,7 +2235,7 @@ let check_unused_names names =
if not (List.is_empty names) && Flags.is_verbose () then
msg_warning
(str"Unused introduction " ++ str (String.plural (List.length names) "pattern")
- ++ str": " ++ prlist_with_sep spc (Miscprint.pr_intro_pattern Printer.pr_constr) names)
+ ++ str": " ++ prlist_with_sep spc (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr (snd (c (Global.env()) Evd.empty)))) names)
let intropattern_of_name gl avoid = function
| Anonymous -> IntroNaming IntroAnonymous
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index cee781a8b..238b95a46 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -107,7 +107,7 @@ val intro_patterns_to : Id.t move_location -> intro_patterns ->
unit Proofview.tactic
val intro_patterns_bound_to : int -> Id.t move_location -> intro_patterns ->
unit Proofview.tactic
-val intro_pattern_to : Id.t move_location -> constr intro_pattern_expr ->
+val intro_pattern_to : Id.t move_location -> delayed_open_constr intro_pattern_expr ->
unit Proofview.tactic
(** Implements user-level "intros", with [] standing for "**" *)
@@ -269,8 +269,7 @@ val simple_induct : quantified_hypothesis -> unit Proofview.tactic
val induction : evars_flag ->
(evar_map * constr with_bindings) induction_arg list ->
constr with_bindings option ->
- intro_pattern_naming_expr located option *
- constr or_and_intro_pattern_expr located option ->
+ intro_pattern_naming option * or_and_intro_pattern option ->
clause option -> unit Proofview.tactic
(** {6 Case analysis tactics. } *)
@@ -282,8 +281,7 @@ val simple_destruct : quantified_hypothesis -> unit Proofview.tactic
val destruct : evars_flag ->
(evar_map * constr with_bindings) induction_arg list ->
constr with_bindings option ->
- intro_pattern_naming_expr located option *
- constr or_and_intro_pattern_expr located option ->
+ intro_pattern_naming option * or_and_intro_pattern option ->
clause option -> unit Proofview.tactic
(** {6 Generic case analysis / induction tactics. } *)
@@ -292,9 +290,7 @@ val destruct : evars_flag ->
val induction_destruct : rec_flag -> evars_flag ->
((evar_map * constr with_bindings) induction_arg *
- (intro_pattern_naming_expr located option *
- constr or_and_intro_pattern_expr located option))
- list *
+ (intro_pattern_naming option * or_and_intro_pattern option)) list *
constr with_bindings option *
clause option -> unit Proofview.tactic
@@ -372,12 +368,12 @@ val cut : types -> unit Proofview.tactic
(** {6 Tactics for adding local definitions. } *)
-val letin_tac : (bool * intro_pattern_naming_expr located) option ->
+val letin_tac : (bool * intro_pattern_naming) option ->
Name.t -> constr -> types option -> clause -> unit Proofview.tactic
(** Common entry point for user-level "set", "pose" and "remember" *)
-val letin_pat_tac : (bool * intro_pattern_naming_expr located) option ->
+val letin_pat_tac : (bool * intro_pattern_naming) option ->
Name.t -> evar_map * constr -> clause -> unit Proofview.tactic
(** {6 Generalize tactics. } *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 09:27:20 +0000