aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/doc/changes.txt4
-rw-r--r--grammar/q_coqast.ml418
-rw-r--r--intf/misctypes.mli12
-rw-r--r--intf/tacexpr.mli10
-rw-r--r--parsing/g_tactic.ml473
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml2
-rw-r--r--plugins/funind/g_indfun.ml47
-rw-r--r--plugins/funind/indfun.mli2
-rw-r--r--plugins/funind/invfun.ml4
-rw-r--r--printing/miscprint.ml18
-rw-r--r--printing/miscprint.mli4
-rw-r--r--printing/pptactic.ml23
-rw-r--r--tactics/elim.ml2
-rw-r--r--tactics/equality.ml4
-rw-r--r--tactics/inv.ml16
-rw-r--r--tactics/inv.mli6
-rw-r--r--tactics/taccoerce.ml21
-rw-r--r--tactics/taccoerce.mli3
-rw-r--r--tactics/tacintern.ml47
-rw-r--r--tactics/tacinterp.ml74
-rw-r--r--tactics/tacticals.ml4
-rw-r--r--tactics/tacticals.mli6
-rw-r--r--tactics/tactics.ml191
-rw-r--r--tactics/tactics.mli27
-rw-r--r--toplevel/auto_ind_decl.ml11
25 files changed, 335 insertions, 254 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 036bf1d5e3..4ea33ddbea 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -87,6 +87,10 @@
- API of Inductiveops made more uniform (see commit log or file itself).
+- API of intros_pattern style tactic changed; "s" is dropped in
+ "intros_pattern" and "intros_patterns" is not anymore behaving like
+ tactic "intros" on the empty list.
+
=========================================
= CHANGES BETWEEN COQ V8.3 AND COQ V8.4 =
=========================================
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 6483f66a3d..2bce95f1e6 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -58,15 +58,21 @@ let mlexpr_of_by_notation f = function
let loc = of_coqloc loc in
<:expr< Misctypes.ByNotation $dloc$ $str:s$ $mlexpr_of_option mlexpr_of_string sco$ >>
-let mlexpr_of_intro_pattern = function
+let mlexpr_of_intro_pattern_disjunctive = function
+ _ -> failwith "mlexpr_of_intro_pattern_disjunctive: TODO"
+
+let mlexpr_of_intro_pattern_naming = function
| Misctypes.IntroWildcard -> <:expr< Misctypes.IntroWildcard >>
| Misctypes.IntroAnonymous -> <:expr< Misctypes.IntroAnonymous >>
| Misctypes.IntroFresh id -> <:expr< Misctypes.IntroFresh (mlexpr_of_ident $dloc$ id) >>
- | Misctypes.IntroForthcoming b -> <:expr< Misctypes.IntroForthcoming (mlexpr_of_bool $dloc$ b) >>
| Misctypes.IntroIdentifier id ->
<:expr< Misctypes.IntroIdentifier (mlexpr_of_ident $dloc$ id) >>
- | Misctypes.IntroOrAndPattern _ | Misctypes.IntroRewrite _
- | Misctypes.IntroInjection _ ->
+
+let mlexpr_of_intro_pattern = function
+ | Misctypes.IntroForthcoming b -> <:expr< Misctypes.IntroForthcoming (mlexpr_of_bool $dloc$ b) >>
+ | Misctypes.IntroNaming pat ->
+ <:expr< Misctypes.IntroNaming $mlexpr_of_intro_pattern_naming pat$ >>
+ | Misctypes.IntroAction _ ->
failwith "mlexpr_of_intro_pattern: TODO"
let mlexpr_of_ident_option = mlexpr_of_option (mlexpr_of_ident)
@@ -366,8 +372,8 @@ let rec mlexpr_of_atomic_tactic = function
(mlexpr_of_option mlexpr_of_bool)
mlexpr_of_induction_arg)
(mlexpr_of_pair
- (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern))
- (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern)))))
+ (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern_naming))
+ (mlexpr_of_option (mlexpr_of_intro_pattern_disjunctive)))))
(mlexpr_of_option mlexpr_of_constr_with_binding)
(mlexpr_of_option mlexpr_of_clause) l$ >>
diff --git a/intf/misctypes.mli b/intf/misctypes.mli
index 6ee44215c0..3d9a344ee9 100644
--- a/intf/misctypes.mli
+++ b/intf/misctypes.mli
@@ -17,14 +17,18 @@ type patvar = Id.t
(** Introduction patterns *)
type intro_pattern_expr =
- | IntroOrAndPattern of or_and_intro_pattern_expr
- | IntroInjection of (Loc.t * intro_pattern_expr) list
+ | IntroForthcoming of bool
+ | IntroNaming of intro_pattern_naming_expr
+ | IntroAction of intro_pattern_action_expr
+and intro_pattern_naming_expr =
| IntroWildcard
- | IntroRewrite of bool
| IntroIdentifier of Id.t
| IntroFresh of Id.t
- | IntroForthcoming of bool
| IntroAnonymous
+and intro_pattern_action_expr =
+ | IntroOrAndPattern of or_and_intro_pattern_expr
+ | IntroInjection of (Loc.t * intro_pattern_expr) list
+ | IntroRewrite of bool
and or_and_intro_pattern_expr = (Loc.t * intro_pattern_expr) list list
(** Move destination for hypothesis *)
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index cf8d34d7e7..2af77eb103 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -44,9 +44,9 @@ type inversion_kind =
type ('c,'id) inversion_strength =
| NonDepInversion of
- inversion_kind * 'id list * intro_pattern_expr located option
+ inversion_kind * 'id list * or_and_intro_pattern_expr located option
| DepInversion of
- inversion_kind * 'c option * intro_pattern_expr located option
+ inversion_kind * 'c option * or_and_intro_pattern_expr located option
| InversionUsing of 'c * 'id list
type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b
@@ -58,8 +58,8 @@ type 'id message_token =
type 'constr induction_clause =
'constr with_bindings induction_arg *
- (intro_pattern_expr located option (* eqn:... *)
- * intro_pattern_expr located option) (* as ... *)
+ (intro_pattern_naming_expr located option (* eqn:... *)
+ * or_and_intro_pattern_expr located option) (* as ... *)
type ('constr,'id) induction_clause_list =
'constr induction_clause list
@@ -127,7 +127,7 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
| TacGeneralize of ('trm with_occurrences * Name.t) list
| TacGeneralizeDep of 'trm
| TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag *
- intro_pattern_expr located option
+ intro_pattern_naming_expr located option
(* Derived basic tactics *)
| TacInductionDestruct of
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 2f9ab38d25..9cf476a5ea 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -274,30 +274,30 @@ GEXTEND Gram
intropatterns:
[ [ l = LIST0 nonsimple_intropattern -> l ]]
;
- disjunctive_intropattern:
- [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> !@loc,IntroOrAndPattern tc
- | "()" -> !@loc,IntroOrAndPattern [[]]
- | "("; si = simple_intropattern; ")" -> !@loc,IntroOrAndPattern [[si]]
+ or_and_intropattern:
+ [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> tc
+ | "()" -> [[]]
+ | "("; si = simple_intropattern; ")" -> [[si]]
| "("; si = simple_intropattern; ",";
- tc = LIST1 simple_intropattern SEP "," ; ")" ->
- !@loc,IntroOrAndPattern [si::tc]
+ tc = LIST1 simple_intropattern SEP "," ; ")" -> [si::tc]
| "("; si = simple_intropattern; "&";
tc = LIST1 simple_intropattern SEP "&" ; ")" ->
(* (A & B & C) is translated into (A,(B,C)) *)
let rec pairify = function
- | ([]|[_]|[_;_]) as l -> IntroOrAndPattern [l]
- | t::q -> IntroOrAndPattern [[t;(loc_of_ne_list q,pairify q)]]
- in !@loc,pairify (si::tc)
- | "[="; tc = intropatterns; "]" -> !@loc,IntroInjection tc
- ] ]
+ | ([]|[_]|[_;_]) as l -> [l]
+ | t::q -> [[t;(loc_of_ne_list q,IntroAction (IntroOrAndPattern (pairify q)))]]
+ in pairify (si::tc) ] ]
+ ;
+ equality_intropattern:
+ [ [ "->" -> IntroRewrite true
+ | "<-" -> IntroRewrite false
+ | "[="; tc = intropatterns; "]" -> IntroInjection tc ] ]
;
naming_intropattern:
- [ [ prefix = pattern_ident -> !@loc, IntroFresh prefix
- | "?" -> !@loc, IntroAnonymous
- | id = ident -> !@loc, IntroIdentifier id
- | "_" -> !@loc, IntroWildcard
- | "->" -> !@loc, IntroRewrite true
- | "<-" -> !@loc, IntroRewrite false ] ]
+ [ [ prefix = pattern_ident -> IntroFresh prefix
+ | "?" -> IntroAnonymous
+ | id = ident -> IntroIdentifier id
+ | "_" -> IntroWildcard ] ]
;
nonsimple_intropattern:
[ [ l = simple_intropattern -> l
@@ -305,8 +305,9 @@ GEXTEND Gram
| "**" -> !@loc, IntroForthcoming false ]]
;
simple_intropattern:
- [ [ pat = disjunctive_intropattern -> pat
- | pat = naming_intropattern -> pat ] ]
+ [ [ pat = or_and_intropattern -> !@loc, IntroAction (IntroOrAndPattern pat)
+ | pat = equality_intropattern -> !@loc, IntroAction pat
+ | pat = naming_intropattern -> !@loc, IntroNaming pat ] ]
;
simple_binding:
[ [ "("; id = ident; ":="; c = lconstr; ")" -> (!@loc, NamedHyp id, c)
@@ -472,15 +473,23 @@ GEXTEND Gram
[ [ "as"; ipat = simple_intropattern -> Some ipat
| -> None ] ]
;
- with_inversion_names:
- [ [ "as"; ipat = simple_intropattern -> Some ipat
+ or_and_intropattern_loc:
+ [ [ ipat = or_and_intropattern -> !@loc, ipat
+ | id = ident ->
+ !@loc,
+ (* coding, see tacinterp.ml: *)
+ [[Loc.ghost, IntroNaming (IntroIdentifier id)]]
+ ] ]
+ ;
+ as_or_and_ipat:
+ [ [ "as"; ipat = or_and_intropattern_loc -> Some ipat
| -> None ] ]
;
eqn_ipat:
- [ [ IDENT "eqn"; ":"; id = naming_intropattern -> Some id
- | IDENT "_eqn"; ":"; id = naming_intropattern ->
+ [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some (!@loc, pat)
+ | IDENT "_eqn"; ":"; pat = naming_intropattern ->
let msg = "Obsolete syntax \"_eqn:H\" could be replaced by \"eqn:H\"" in
- msg_warning (strbrk msg); Some id
+ msg_warning (strbrk msg); Some (!@loc, pat)
| IDENT "_eqn" ->
let msg = "Obsolete syntax \"_eqn\" could be replaced by \"eqn:?\"" in
msg_warning (strbrk msg); Some (!@loc, IntroAnonymous)
@@ -513,7 +522,7 @@ GEXTEND Gram
[ [ b = orient; p = rewriter -> let (m,c) = p in (b,m,c) ] ]
;
induction_clause:
- [ [ c = induction_arg; pat = as_ipat; eq = eqn_ipat -> (c,(eq,pat)) ] ]
+ [ [ c = induction_arg; pat = as_or_and_ipat; eq = eqn_ipat -> (c,(eq,pat)) ] ]
;
induction_clause_list:
[ [ ic = LIST1 induction_clause SEP ",";
@@ -577,17 +586,17 @@ GEXTEND Gram
(* Alternative syntax for "pose proof c as id" *)
| IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":=";
c = lconstr; ")" ->
- TacAtom (!@loc, TacAssert (true,None,Some (!@loc,IntroIdentifier id),c))
+ TacAtom (!@loc, TacAssert (true,None,Some (!@loc,IntroNaming (IntroIdentifier id)),c))
(* Alternative syntax for "assert c as id by tac" *)
| IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
c = lconstr; ")"; tac=by_tactic ->
- TacAtom (!@loc, TacAssert (true,Some tac,Some (!@loc,IntroIdentifier id),c))
+ TacAtom (!@loc, TacAssert (true,Some tac,Some (!@loc,IntroNaming (IntroIdentifier id)),c))
(* Alternative syntax for "enough c as id by tac" *)
| IDENT "enough"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
c = lconstr; ")"; tac=by_tactic ->
- TacAtom (!@loc, TacAssert (false,Some tac,Some (!@loc,IntroIdentifier id),c))
+ TacAtom (!@loc, TacAssert (false,Some tac,Some (!@loc,IntroNaming (IntroIdentifier id)),c))
| IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic ->
TacAtom (!@loc, TacAssert (true,Some tac,ipat,c))
@@ -654,18 +663,18 @@ GEXTEND Gram
| IDENT "inversion" -> FullInversion
| IDENT "inversion_clear" -> FullInversionClear ];
hyp = quantified_hypothesis;
- ids = with_inversion_names; co = OPT ["with"; c = constr -> c] ->
+ ids = as_or_and_ipat; co = OPT ["with"; c = constr -> c] ->
TacAtom (!@loc, TacInversion (DepInversion (k,co,ids),hyp))
| IDENT "simple"; IDENT "inversion";
- hyp = quantified_hypothesis; ids = with_inversion_names;
+ hyp = quantified_hypothesis; ids = as_or_and_ipat;
cl = in_hyp_list ->
TacAtom (!@loc, TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp))
| IDENT "inversion";
- hyp = quantified_hypothesis; ids = with_inversion_names;
+ hyp = quantified_hypothesis; ids = as_or_and_ipat;
cl = in_hyp_list ->
TacAtom (!@loc, TacInversion (NonDepInversion (FullInversion, cl, ids), hyp))
| IDENT "inversion_clear";
- hyp = quantified_hypothesis; ids = with_inversion_names;
+ hyp = quantified_hypothesis; ids = as_or_and_ipat;
cl = in_hyp_list ->
TacAtom (!@loc, TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp))
| IDENT "inversion"; hyp = quantified_hypothesis;
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index f780d1bb50..702d554fc5 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -735,7 +735,7 @@ let consider_tac c hyps gls =
| _ ->
let id = pf_get_new_id (Id.of_string "_tmp") gls in
tclTHEN
- (Proofview.V82.of_tactic (forward true None (Some (Loc.ghost, IntroIdentifier id)) c))
+ (Proofview.V82.of_tactic (pose_proof (Name id) c))
(consider_match false [] [id] hyps) gls
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index d77385321e..5fa689f000 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -83,6 +83,9 @@ let pr_intro_as_pat prc _ _ pat =
spc () ++ str "as" ++ spc () ++ Miscprint.pr_intro_pattern pat
| None -> mt ()
+let out_disjunctive = function
+ | loc, IntroAction (IntroOrAndPattern l) -> (loc,l)
+ | _ -> Errors.error "Disjunctive or conjunctive intro pattern expected."
ARGUMENT EXTEND with_names TYPED AS simple_intropattern_opt PRINTED BY pr_intro_as_pat
| [ "as" simple_intropattern(ipat) ] -> [ Some ipat ]
@@ -100,7 +103,7 @@ TACTIC EXTEND newfunind
| [c] -> c
| c::cl -> applist(c,cl)
in
- Extratactics.onSomeWithHoles (fun x -> Proofview.V82.tactic (functional_induction true c x pat)) princl ]
+ Extratactics.onSomeWithHoles (fun x -> Proofview.V82.tactic (functional_induction true c x (Option.map out_disjunctive pat))) princl ]
END
(***** debug only ***)
TACTIC EXTEND snewfunind
@@ -111,7 +114,7 @@ TACTIC EXTEND snewfunind
| [c] -> c
| c::cl -> applist(c,cl)
in
- Extratactics.onSomeWithHoles (fun x -> Proofview.V82.tactic (functional_induction false c x pat)) princl ]
+ Extratactics.onSomeWithHoles (fun x -> Proofview.V82.tactic (functional_induction false c x (Option.map out_disjunctive pat))) princl ]
END
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index 91a5ddf826..f88a72ff51 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 ->
- intro_pattern_expr Loc.located option ->
+ or_and_intro_pattern_expr Loc.located option ->
Proof_type.goal Tacmach.sigma -> Proof_type.goal list Evd.sigma
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 4fcc65bda9..97157facd0 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -271,7 +271,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
List.map
(fun (_,_,br_type) ->
List.map
- (fun id -> Loc.ghost, IntroIdentifier id)
+ (fun id -> Loc.ghost, IntroNaming (IntroIdentifier id))
(generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum br_type))))
)
branches
@@ -329,7 +329,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
List.fold_right
(fun (_,pat) acc ->
match pat with
- | IntroIdentifier id -> id::acc
+ | IntroNaming (IntroIdentifier id) -> id::acc
| _ -> anomaly (Pp.str "Not an identifier")
)
(List.nth intro_pats (pred i))
diff --git a/printing/miscprint.ml b/printing/miscprint.ml
index 3a0f7a8f75..3193a74a04 100644
--- a/printing/miscprint.ml
+++ b/printing/miscprint.ml
@@ -12,17 +12,23 @@ open Pp
(** Printing of [intro_pattern] *)
let rec pr_intro_pattern (_,pat) = match pat with
+ | IntroForthcoming true -> str "*"
+ | IntroForthcoming false -> str "**"
+ | IntroNaming p -> pr_intro_pattern_naming p
+ | IntroAction p -> pr_intro_pattern_action p
+
+and pr_intro_pattern_naming = function
+ | IntroWildcard -> str "_"
+ | IntroIdentifier id -> Nameops.pr_id id
+ | IntroFresh id -> str "?" ++ Nameops.pr_id id
+ | IntroAnonymous -> str "?"
+
+and pr_intro_pattern_action = function
| IntroOrAndPattern pll -> pr_or_and_intro_pattern pll
| IntroInjection pl ->
str "[=" ++ hv 0 (prlist_with_sep spc pr_intro_pattern pl) ++ str "]"
- | IntroWildcard -> str "_"
| IntroRewrite true -> str "->"
| IntroRewrite false -> str "<-"
- | IntroIdentifier id -> Nameops.pr_id id
- | IntroFresh id -> str "?" ++ Nameops.pr_id id
- | IntroForthcoming true -> str "*"
- | IntroForthcoming false -> str "**"
- | IntroAnonymous -> str "?"
and pr_or_and_intro_pattern = function
| [pl] ->
diff --git a/printing/miscprint.mli b/printing/miscprint.mli
index 4e0be83f24..d242bad3ac 100644
--- a/printing/miscprint.mli
+++ b/printing/miscprint.mli
@@ -12,6 +12,10 @@ open Misctypes
val pr_intro_pattern : intro_pattern_expr Loc.located -> Pp.std_ppcmds
+val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds
+
+val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.std_ppcmds
+
(** Printing of [move_location] *)
val pr_move_location :
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 785b0e8dce..3caee02de5 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -347,26 +347,23 @@ let pr_bindings prc prlc = pr_bindings_gen false prc prlc
let pr_with_bindings prc prlc (c,bl) =
hov 1 (prc c ++ pr_bindings prc prlc bl)
-let pr_as_ipat pat = str "as " ++ Miscprint.pr_intro_pattern pat
-let pr_eqn_ipat pat = str "eqn:" ++ Miscprint.pr_intro_pattern pat
+let pr_as_disjunctive_ipat (_,ipatl) =
+ str "as " ++ Miscprint.pr_or_and_intro_pattern ipatl
+let pr_eqn_ipat (_,ipat) = str "eqn:" ++ Miscprint.pr_intro_pattern_naming ipat
+let pr_as_ipat = function
+ | None -> mt ()
+ | Some ipat -> str "as " ++ Miscprint.pr_intro_pattern ipat
let pr_with_induction_names = function
| None, None -> mt ()
| Some eqpat, None -> spc () ++ hov 1 (pr_eqn_ipat eqpat)
- | None, Some ipat -> spc () ++ hov 1 (pr_as_ipat ipat)
+ | None, Some ipat -> spc () ++ hov 1 (pr_as_disjunctive_ipat ipat)
| Some eqpat, Some ipat ->
- spc () ++ hov 1 (pr_as_ipat ipat ++ spc () ++ pr_eqn_ipat eqpat)
-
-let pr_as_intro_pattern ipat =
- spc () ++ hov 1 (str "as" ++ spc () ++ Miscprint.pr_intro_pattern ipat)
+ spc () ++ hov 1 (pr_as_disjunctive_ipat ipat ++ spc () ++ pr_eqn_ipat eqpat)
let pr_with_inversion_names = function
| None -> mt ()
- | Some ipat -> pr_as_intro_pattern ipat
-
-let pr_as_ipat = function
- | None -> mt ()
- | Some ipat -> pr_as_intro_pattern ipat
+ | Some ipat -> pr_as_disjunctive_ipat ipat
let pr_as_name = function
| Anonymous -> mt ()
@@ -390,7 +387,7 @@ let pr_assertion prc _prlc ipat c = match ipat with
let pr_assumption prc prlc ipat c = match ipat with
(* Use this "optimisation" or use only the general case ?*)
(* it seems that this "optimisation" is somehow more natural *)
- | Some (_,IntroIdentifier id) ->
+ | Some (_,IntroNaming (IntroIdentifier id)) ->
spc() ++ surround (pr_id id ++ str " :" ++ spc() ++ prlc c)
| ipat ->
spc() ++ prc c ++ pr_as_ipat ipat
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 2a7b3bff1c..2bedf2a4c6 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -41,7 +41,7 @@ let introCaseAssumsThen tac ba =
(ba.Tacticals.branchnames, []),
if n1 > n2 then snd (List.chop n2 case_thin_sign) else [] in
let introCaseAssums =
- tclTHEN (intros_pattern MoveLast l1) (intros_clearing l3) in
+ tclTHEN (intro_patterns l1) (intros_clearing l3) in
(tclTHEN introCaseAssums (case_on_ba (tac l2) ba))
(* The following tactic Decompose repeatedly applies the
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 56a5920a14..5f8e9f5030 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1320,8 +1320,8 @@ let postInjEqTac clear_flag ipats c n =
tclTRY (apply_clear_request clear_flag dft c) in
let intro_tac =
if use_injection_pattern_l2r_order ()
- then intros_pattern_bound n MoveLast ipats
- else intros_pattern MoveLast ipats in
+ then intro_patterns_bound_to n MoveLast ipats
+ else intro_patterns_to MoveLast ipats in
tclTHEN clear_tac intro_tac
| None -> tclIDTAC
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 5b3f7374cc..45f416c2cf 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -375,15 +375,15 @@ let rewrite_equations_gene othin neqns ba =
Some thin: the equations are rewritten, and cleared if thin is true *)
let rec get_names allow_conj (loc,pat) = match pat with
- | IntroWildcard ->
+ | IntroNaming IntroWildcard ->
error "Discarding pattern not allowed for inversion equations."
- | IntroAnonymous | IntroForthcoming _ ->
+ | IntroNaming IntroAnonymous | IntroForthcoming _ ->
error "Anonymous pattern not allowed for inversion equations."
- | IntroFresh _ ->
+ | IntroNaming (IntroFresh _) ->
error "Fresh pattern not allowed for inversion equations."
- | IntroRewrite _->
+ | IntroAction (IntroRewrite _) ->
error "Rewriting pattern not allowed for inversion equations."
- | IntroOrAndPattern [l] ->
+ | IntroAction (IntroOrAndPattern [l]) ->
let get_name id = Option.get (fst (get_names false id)) in
if allow_conj then begin match l with
| [] -> (None, [])
@@ -392,11 +392,11 @@ let rec get_names allow_conj (loc,pat) = match pat with
(Some n, n :: List.map get_name l)
end else
error"Nested conjunctive patterns not allowed for inversion equations."
- | IntroInjection l ->
+ | IntroAction (IntroInjection l) ->
error "Injection patterns not allowed for inversion equations."
- | IntroOrAndPattern l ->
+ | IntroAction (IntroOrAndPattern l) ->
error "Disjunctive patterns not allowed for inversion equations."
- | IntroIdentifier id ->
+ | IntroNaming (IntroIdentifier id) ->
(Some id,[id])
let extract_eqn_names = function
diff --git a/tactics/inv.mli b/tactics/inv.mli
index 615ceaab56..7416d29bb1 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 -> intro_pattern_expr located option -> Id.t list ->
+ inversion_kind -> or_and_intro_pattern_expr located option -> Id.t list ->
quantified_hypothesis -> unit Proofview.tactic
-val inv : inversion_kind -> intro_pattern_expr located option ->
+val inv : inversion_kind -> or_and_intro_pattern_expr located option ->
quantified_hypothesis -> unit Proofview.tactic
val dinv : inversion_kind -> constr option ->
- intro_pattern_expr located option -> quantified_hypothesis -> unit Proofview.tactic
+ or_and_intro_pattern_expr located 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.ml b/tactics/taccoerce.ml
index c1f9fe30d9..a88268621a 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -89,7 +89,7 @@ let coerce_to_ident fresh env v =
let fail () = raise (CannotCoerceTo "a fresh identifier") in
if has_type v (topwit wit_intro_pattern) then
match out_gen (topwit wit_intro_pattern) v with
- | _, IntroIdentifier id -> id
+ | _, IntroNaming (IntroIdentifier id) -> id
| _ -> fail ()
else if has_type v (topwit wit_var) then
out_gen (topwit wit_var) v
@@ -107,19 +107,24 @@ let coerce_to_intro_pattern env v =
snd (out_gen (topwit wit_intro_pattern) v)
else if has_type v (topwit wit_var) then
let id = out_gen (topwit wit_var) v in
- IntroIdentifier id
+ IntroNaming (IntroIdentifier id)
else match Value.to_constr v with
| Some c when isVar c ->
(* This happens e.g. in definitions like "Tac H = clear H; intro H" *)
(* but also in "destruct H as (H,H')" *)
- IntroIdentifier (destVar c)
+ IntroNaming (IntroIdentifier (destVar c))
| _ -> raise (CannotCoerceTo "an introduction pattern")
+let coerce_to_intro_pattern_naming env v =
+ match coerce_to_intro_pattern env v with
+ | IntroNaming pat -> pat
+ | _ -> raise (CannotCoerceTo "a naming introduction pattern")
+
let coerce_to_hint_base v =
let v = Value.normalize v in
if has_type v (topwit wit_intro_pattern) then
match out_gen (topwit wit_intro_pattern) v with
- | _, IntroIdentifier id -> Id.to_string id
+ | _, IntroNaming (IntroIdentifier id) -> Id.to_string id
| _ -> raise (CannotCoerceTo "a hint base name")
else raise (CannotCoerceTo "a hint base name")
@@ -134,7 +139,7 @@ let coerce_to_constr env v =
let fail () = raise (CannotCoerceTo "a term") in
if has_type v (topwit wit_intro_pattern) then
match out_gen (topwit wit_intro_pattern) v with
- | _, IntroIdentifier id ->
+ | _, IntroNaming (IntroIdentifier id) ->
(try ([], constr_of_id env id) with Not_found -> fail ())
| _ -> fail ()
else if has_type v (topwit wit_constr) then
@@ -164,7 +169,7 @@ let coerce_to_evaluable_ref env v =
let v = Value.normalize v in
if has_type v (topwit wit_intro_pattern) then
match out_gen (topwit wit_intro_pattern) v with
- | _, IntroIdentifier id when is_variable env id -> EvalVarRef id
+ | _, IntroNaming (IntroIdentifier id) when is_variable env id -> EvalVarRef id
| _ -> fail ()
else if has_type v (topwit wit_var) then
let id = out_gen (topwit wit_var) v in
@@ -198,7 +203,7 @@ let coerce_to_hyp env v =
let v = Value.normalize v in
if has_type v (topwit wit_intro_pattern) then
match out_gen (topwit wit_intro_pattern) v with
- | _, IntroIdentifier id when is_variable env id -> id
+ | _, IntroNaming (IntroIdentifier id) when is_variable env id -> id
| _ -> fail ()
else if has_type v (topwit wit_var) then
let id = out_gen (topwit wit_var) v in
@@ -238,7 +243,7 @@ let coerce_to_quantified_hypothesis v =
if has_type v (topwit wit_intro_pattern) then
let v = out_gen (topwit wit_intro_pattern) v in
match v with
- | _, IntroIdentifier id -> NamedHyp id
+ | _, IntroNaming (IntroIdentifier id) -> NamedHyp id
| _ -> raise (CannotCoerceTo "a quantified hypothesis")
else if has_type v (topwit wit_var) then
let id = out_gen (topwit wit_var) v in
diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli
index 7b278996e0..f2b3b225b5 100644
--- a/tactics/taccoerce.mli
+++ b/tactics/taccoerce.mli
@@ -52,6 +52,9 @@ val coerce_to_ident : bool -> Environ.env -> Value.t -> Id.t
val coerce_to_intro_pattern : Environ.env -> Value.t -> intro_pattern_expr
+val coerce_to_intro_pattern_naming :
+ Environ.env -> Value.t -> intro_pattern_naming_expr
+
val coerce_to_hint_base : Value.t -> string
val coerce_to_int : Value.t -> int
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 4a4368404f..0d086d842d 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -203,7 +203,7 @@ let intern_non_tactic_reference strict ist r =
(* By convention, use IntroIdentifier for unbound ident, when not in a def *)
match r with
| Ident (loc,id) when not strict ->
- let ipat = in_gen (glbwit wit_intro_pattern) (loc, IntroIdentifier id) in
+ let ipat = in_gen (glbwit wit_intro_pattern) (loc, IntroNaming (IntroIdentifier id)) in
TacGeneric ipat
| _ ->
(* Reference not found *)
@@ -216,20 +216,35 @@ let intern_message_token ist = function
let intern_message ist = List.map (intern_message_token ist)
let rec intern_intro_pattern lf ist = function
- | loc, IntroOrAndPattern l ->
- loc, IntroOrAndPattern (intern_or_and_intro_pattern lf ist l)
- | loc, IntroInjection l ->
- loc, IntroInjection (List.map (intern_intro_pattern lf ist) l)
- | loc, IntroIdentifier id ->
- loc, IntroIdentifier (intern_ident lf ist id)
- | loc, IntroFresh id ->
- loc, IntroFresh (intern_ident lf ist id)
- | loc, (IntroWildcard | IntroAnonymous | IntroRewrite _ | IntroForthcoming _)
- as x -> x
+ | loc, IntroNaming pat ->
+ loc, IntroNaming (intern_intro_pattern_naming lf ist pat)
+ | loc, IntroAction pat ->
+ loc, IntroAction (intern_intro_pattern_action lf ist pat)
+ | loc, IntroForthcoming _ as x -> x
+
+and intern_intro_pattern_naming lf ist = function
+ | IntroIdentifier id ->
+ IntroIdentifier (intern_ident lf ist id)
+ | IntroFresh id ->
+ IntroFresh (intern_ident lf ist id)
+ | IntroWildcard | IntroAnonymous as x -> x
+
+and intern_intro_pattern_action lf ist = function
+ | IntroOrAndPattern l ->
+ IntroOrAndPattern (intern_or_and_intro_pattern lf ist l)
+ | IntroInjection l ->
+ IntroInjection (List.map (intern_intro_pattern lf ist) l)
+ | IntroRewrite _ as x -> x
and intern_or_and_intro_pattern lf ist =
List.map (List.map (intern_intro_pattern lf ist))
+let intern_or_and_intro_pattern_loc lf ist (loc,l) =
+ (loc,intern_or_and_intro_pattern lf ist l)
+
+let intern_intro_pattern_naming_loc lf ist (loc,pat) =
+ (loc,intern_intro_pattern_naming lf ist pat)
+
let intern_quantified_hypothesis ist = function
| AnonHyp n -> AnonHyp n
| NamedHyp id ->
@@ -380,10 +395,10 @@ let intern_hyp_list ist = List.map (intern_hyp ist)
let intern_inversion_strength lf ist = function
| NonDepInversion (k,idl,ids) ->
NonDepInversion (k,intern_hyp_list ist idl,
- Option.map (intern_intro_pattern lf ist) ids)
+ Option.map (intern_or_and_intro_pattern_loc lf ist) ids)
| DepInversion (k,copt,ids) ->
DepInversion (k, Option.map (intern_constr ist) copt,
- Option.map (intern_intro_pattern lf ist) ids)
+ Option.map (intern_or_and_intro_pattern_loc lf ist) ids)
| InversionUsing (c,idl) ->
InversionUsing (intern_constr ist c, intern_hyp_list ist idl)
@@ -486,7 +501,7 @@ let rec intern_atomic lf ist x =
let na = intern_name lf ist na in
TacLetTac (na,intern_constr ist c,
(clause_app (intern_hyp_location ist) cls),b,
- (Option.map (intern_intro_pattern lf ist) eqpat))
+ (Option.map (intern_intro_pattern_naming_loc lf ist) eqpat))
(* Automation tactics *)
| TacTrivial (d,lems,l) -> TacTrivial (d,List.map (intern_constr ist) lems,l)
@@ -498,8 +513,8 @@ let rec intern_atomic lf ist x =
| TacInductionDestruct (ev,isrec,(l,el,cls)) ->
TacInductionDestruct (ev,isrec,(List.map (fun (c,(ipato,ipats)) ->
(intern_induction_arg ist c,
- (Option.map (intern_intro_pattern lf ist) ipato,
- Option.map (intern_intro_pattern lf ist) ipats))) l,
+ (Option.map (intern_intro_pattern_naming_loc lf ist) ipato,
+ Option.map (intern_or_and_intro_pattern_loc lf ist) ipats))) l,
Option.map (intern_constr_with_bindings ist) el,
Option.map (clause_app (intern_hyp_location ist)) cls))
| TacDoubleInduction (h1,h2) ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 02e49584f3..a4f9ba2d78 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -231,7 +231,8 @@ let extern_request ch req gl la =
output_string ch "</REQUEST>\n"
let value_of_ident id =
- in_gen (topwit wit_intro_pattern) (Loc.ghost, IntroIdentifier id)
+ in_gen (topwit wit_intro_pattern)
+ (Loc.ghost, IntroNaming (IntroIdentifier id))
let (+++) lfun1 lfun2 = Id.Map.fold Id.Map.add lfun1 lfun2
@@ -302,6 +303,10 @@ let interp_fresh_name ist env = function
let interp_intro_pattern_var loc ist env id =
try try_interp_ltac_var (coerce_to_intro_pattern env) ist (Some env) (loc,id)
+ with Not_found -> IntroNaming (IntroIdentifier id)
+
+let interp_intro_pattern_naming_var loc ist env id =
+ try try_interp_ltac_var (coerce_to_intro_pattern_naming env) ist (Some env) (loc,id)
with Not_found -> IntroIdentifier id
let interp_hint_base ist s =
@@ -415,12 +420,13 @@ let extract_ltac_constr_values ist env =
(* Extract the identifier list from lfun: join all branches (what to do else?)*)
let rec intropattern_ids (loc,pat) = match pat with
- | IntroIdentifier id -> [id]
- | IntroOrAndPattern ll ->
+ | IntroNaming (IntroIdentifier id) -> [id]
+ | IntroAction (IntroOrAndPattern ll) ->
List.flatten (List.map intropattern_ids (List.flatten ll))
- | IntroInjection l ->
+ | IntroAction (IntroInjection l) ->
List.flatten (List.map intropattern_ids l)
- | IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _
+ | IntroNaming (IntroWildcard | IntroAnonymous | IntroFresh _)
+ | IntroAction (IntroRewrite _)
| IntroForthcoming _ -> []
let extract_ids ids lfun =
@@ -747,27 +753,46 @@ let interp_message ist gl l =
prlist_with_sep spc (interp_message_token ist gl) l
let rec interp_intro_pattern ist env = function
- | loc, IntroOrAndPattern l ->
- loc, IntroOrAndPattern (interp_or_and_intro_pattern ist env l)
- | loc, IntroInjection l ->
- loc, IntroInjection (interp_intro_pattern_list_as_list ist env l)
- | loc, IntroIdentifier id ->
+ | loc, IntroAction pat ->
+ loc, IntroAction (interp_intro_pattern_action ist env pat)
+ | loc, IntroNaming (IntroIdentifier id) ->
loc, interp_intro_pattern_var loc ist env id
- | loc, IntroFresh id ->
- loc, IntroFresh (interp_fresh_ident ist env id)
- | loc, (IntroWildcard | IntroAnonymous | IntroRewrite _ | IntroForthcoming _)
- as x -> x
+ | loc, IntroNaming pat ->
+ loc, IntroNaming (snd (interp_intro_pattern_naming ist env (loc,pat)))
+ | loc, IntroForthcoming _ as x -> x
+
+and interp_intro_pattern_naming ist env = function
+ | loc,IntroFresh id -> loc,IntroFresh (interp_fresh_ident ist env id)
+ | loc,IntroIdentifier id -> loc,interp_intro_pattern_naming_var loc ist env id
+ | loc,(IntroWildcard | IntroAnonymous) as x -> x
+
+and interp_intro_pattern_action ist env = function
+ | IntroOrAndPattern l ->
+ IntroOrAndPattern (interp_or_and_intro_pattern ist env l)
+ | IntroInjection l ->
+ IntroInjection (interp_intro_pattern_list_as_list ist env l)
+ | IntroRewrite _ as x -> x
and interp_or_and_intro_pattern ist env =
List.map (interp_intro_pattern_list_as_list ist env)
and interp_intro_pattern_list_as_list ist env = function
- | [loc,IntroIdentifier id] as l ->
+ | [loc,IntroNaming (IntroIdentifier id)] as l ->
(try coerce_to_intro_pattern_list loc env (Id.Map.find id ist.lfun)
with Not_found | CannotCoerceTo _ ->
List.map (interp_intro_pattern ist env) l)
| l -> List.map (interp_intro_pattern ist env) l
+let interp_or_and_intro_pattern_loc ist env (loc,l) =
+ match l with
+ | [[loc',IntroNaming (IntroIdentifier id)]] when (* Hack, see g_tactic.ml4 *) loc' = dloc ->
+ (match coerce_to_intro_pattern env (Id.Map.find id ist.lfun) with
+ | IntroAction (IntroOrAndPattern l) -> (loc,l)
+ | _ ->
+ raise (CannotCoerceTo "a disjunctive/conjunctive introduction pattern"))
+ | l ->
+ (loc,interp_or_and_intro_pattern ist env l)
+
let interp_in_hyp_as ist env (clear,id,ipat) =
(clear,interp_hyp ist env id,Option.map (interp_intro_pattern ist env) ipat)
@@ -868,7 +893,7 @@ let interp_induction_arg ist gl arg =
if has_type v (topwit wit_intro_pattern) then
let v = out_gen (topwit wit_intro_pattern) v in
match v with
- | _, IntroIdentifier id -> try_cast_id id
+ | _, IntroNaming (IntroIdentifier id) -> try_cast_id id
| _ -> error ()
else if has_type v (topwit wit_var) then
let id = out_gen (topwit wit_var) v in
@@ -1313,7 +1338,7 @@ and interp_tacarg ist arg : typed_generic_argument GTac.t =
| TacFreshId l ->
GTac.raw_enter begin fun gl ->
let id = interp_fresh_id ist (Tacmach.New.pf_env gl) l in
- GTac.return (in_gen (topwit wit_intro_pattern) (dloc, IntroIdentifier id))
+ GTac.return (in_gen (topwit wit_intro_pattern) (dloc, IntroNaming (IntroIdentifier id)))
end
| TacPretype c ->
GTac.raw_enter begin fun gl ->
@@ -1667,7 +1692,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
Proofview.Goal.raw_enter begin fun gl ->
let env = Proofview.Goal.env gl in
let patterns = interp_intro_pattern_list_as_list ist env l in
- Tactics.intro_patterns patterns
+ Tactics.intros_patterns patterns
end
| TacIntroMove (ido,hto) ->
Proofview.Goal.raw_enter begin fun gl ->
@@ -1784,7 +1809,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let clp = interp_clause ist env clp in
- let eqpat = Option.map (interp_intro_pattern ist env) eqpat in
+ let eqpat = Option.map (interp_intro_pattern_naming ist env) eqpat in
if Locusops.is_nowhere clp then
(* We try to fully-typecheck the term *)
let (sigma,c_interp) =
@@ -1837,10 +1862,11 @@ and interp_atomic ist tac : unit Proofview.tactic =
let l =
List.map begin fun (c,(ipato,ipats)) ->
let c = Tacmach.New.of_old (fun gl -> interp_induction_arg ist gl c) gl in
- let interp_intro_pattern = interp_intro_pattern ist env in
+ let interp_intro_pattern1 = interp_intro_pattern_naming ist env in
+ let interp_intro_pattern2 = interp_or_and_intro_pattern_loc ist env in
c,
- (Option.map interp_intro_pattern ipato,
- Option.map interp_intro_pattern ipats)
+ (Option.map interp_intro_pattern1 ipato,
+ Option.map interp_intro_pattern2 ipats)
end l
in
let sigma = Proofview.Goal.sigma gl in
@@ -1978,7 +2004,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
in
sigma , Some c_interp
in
- let interp_intro_pattern = interp_intro_pattern ist env in
+ let interp_intro_pattern = interp_or_and_intro_pattern_loc ist env in
let dqhyps = interp_declared_or_quantified_hypothesis ist env hyp in
Inv.dinv k c_interp
(Option.map interp_intro_pattern ids)
@@ -1987,7 +2013,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacInversion (NonDepInversion (k,idl,ids),hyp) ->
Proofview.Goal.raw_enter begin fun gl ->
let env = Proofview.Goal.env gl in
- let interp_intro_pattern = interp_intro_pattern ist env in
+ let interp_intro_pattern = interp_or_and_intro_pattern_loc ist env in
let hyps = interp_hyp_list ist env idl in
let dqhyps = interp_declared_or_quantified_hypothesis ist env hyp in
Inv.inv_clause k
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 0c934bde08..662d02a93e 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -177,12 +177,10 @@ let check_or_and_pattern_size loc names n =
let compute_induction_names n = function
| None ->
Array.make n []
- | Some (loc,IntroOrAndPattern names) ->
+ | Some (loc,names) ->
let names = fix_empty_or_and_pattern n names in
check_or_and_pattern_size loc names n;
Array.of_list names
- | Some (loc,_) ->
- user_err_loc (loc,"",str "Disjunctive/conjunctive introduction pattern expected.")
let compute_construtor_signatures isrec ((_,k as ity),u) =
let rec analrec c recargs =
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 9c91638cfd..ebe1667f24 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -125,7 +125,7 @@ val fix_empty_or_and_pattern : int -> or_and_intro_pattern_expr ->
(** Useful for [as intro_pattern] modifier *)
val compute_induction_names :
- int -> intro_pattern_expr located option ->
+ int -> or_and_intro_pattern_expr located option ->
intro_pattern_expr located list array
val elimination_sort_of_goal : goal sigma -> sorts_family
@@ -242,11 +242,11 @@ module New : sig
constr -> unit Proofview.tactic
val case_then_using :
- intro_pattern_expr located option -> (branch_args -> unit Proofview.tactic) ->
+ or_and_intro_pattern_expr located option -> (branch_args -> unit Proofview.tactic) ->
constr option -> pinductive -> Term.constr * Term.types -> unit Proofview.tactic
val case_nodep_then_using :
- intro_pattern_expr located option -> (branch_args -> unit Proofview.tactic) ->
+ or_and_intro_pattern_expr located 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 c82db8531d..0b9f722fad 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1630,7 +1630,8 @@ let (forward_subst_one, subst_one) = Hook.make ()
let error_unexpected_extra_pattern loc bound pat =
let _,nb = Option.get bound in
let s1,s2,s3 = match pat with
- | IntroIdentifier _ -> "name", (String.plural nb " introduction pattern"), "no"
+ | IntroNaming (IntroIdentifier _) ->
+ "name", (String.plural nb " introduction pattern"), "no"
| _ -> "introduction pattern", "", "none" in
user_err_loc (loc,"",str "Unexpected " ++ str s1 ++ str " (" ++
(if Int.equal nb 0 then (str s3 ++ str s2) else
@@ -1674,13 +1675,16 @@ let intro_or_and_pattern loc bracketed ll thin tac id =
nv (Array.of_list ll))
end
-let rewrite_hyp l2r id =
+let rewrite_hyp assert_style l2r id =
let rew_on l2r =
Hook.get forward_general_multi_rewrite l2r false (mkVar id,NoBindings) in
let subst_on l2r x rhs =
Hook.get forward_subst_one true x (id,rhs,l2r) in
let clear_var_and_eq c =
tclTRY (tclTHEN (clear [id]) (tclTRY (clear [destVar c]))) in
+ if assert_style then
+ rew_on l2r allHypsAndConcl
+ else
Proofview.Goal.raw_enter begin fun gl ->
let env = Proofview.Goal.env gl in
let type_of = Tacmach.New.pf_type_of gl in
@@ -1706,16 +1710,16 @@ let rewrite_hyp l2r id =
end
let rec explicit_intro_names = function
-| (_, IntroIdentifier id) :: l ->
- id :: explicit_intro_names l
-| (_, (IntroWildcard | IntroAnonymous | IntroFresh _
- | IntroRewrite _ | IntroForthcoming _)) :: l -> explicit_intro_names l
-| (_, IntroOrAndPattern ll) :: l' ->
+| (_, IntroForthcoming _) :: l -> explicit_intro_names l
+| (_, IntroNaming (IntroIdentifier id)) :: l -> id :: explicit_intro_names l
+| (_, IntroAction (IntroOrAndPattern ll)) :: l' ->
List.flatten (List.map (fun l -> explicit_intro_names (l@l')) ll)
-| (_, IntroInjection l) :: l' ->
+| (_, IntroAction (IntroInjection l)) :: l' ->
explicit_intro_names (l@l')
-| [] ->
- []
+| (_, (IntroNaming (IntroWildcard | IntroAnonymous | IntroFresh _)
+ | IntroAction (IntroRewrite _))) :: l ->
+ explicit_intro_names l
+| [] -> []
let wild_id = Id.of_string "_tmp"
@@ -1744,55 +1748,64 @@ let exceed_bound n = function
to ensure that dependent hypotheses are cleared in the right
dependency order (see bug #1000); we use fresh names, not used in
the tactic, for the hyps to clear *)
-let rec intros_patterns b avoid ids thin destopt bound n tac = function
- | [] when fit_bound n bound -> tac ids thin
+let rec intro_patterns_core b avoid ids thin destopt bound n tac = function
+ | [] when fit_bound n bound ->
+ tac ids thin
| [] ->
(* Behave as IntroAnonymous *)
- intro_then_gen (NamingAvoid avoid)
- destopt true false
- (fun id -> intros_patterns b avoid (id::ids) thin destopt bound (n+1) tac [])
+ intro_patterns_core b avoid ids thin destopt bound n tac
+ [dloc,IntroNaming IntroAnonymous]
| (loc,pat) :: l ->
if exceed_bound n bound then error_unexpected_extra_pattern loc bound pat else
match pat with
+ | IntroForthcoming onlydeps ->
+ intro_forthcoming_then_gen (NamingAvoid (avoid@explicit_intro_names l))
+ destopt onlydeps n bound
+ (fun ids -> intro_patterns_core b avoid ids thin destopt bound
+ (n+List.length ids) tac l)
+ | IntroAction pat ->
+ intro_then_gen (NamingAvoid(avoid@explicit_intro_names l))
+ MoveLast true false
+ (intro_pattern_action loc (b || not (List.is_empty l)) false pat thin
+ (fun thin bound' -> intro_patterns_core b avoid ids thin destopt bound' 0
+ (fun ids thin ->
+ intro_patterns_core b avoid ids thin destopt bound (n+1) tac l)))
+ | IntroNaming pat ->
+ intro_pattern_naming loc b avoid ids pat thin destopt bound n tac l
+
+and intro_pattern_naming loc b avoid ids pat thin destopt bound n tac l =
+ match pat with
| IntroWildcard ->
intro_then_gen (NamingBasedOn(wild_id,avoid@explicit_intro_names l))
MoveLast true false
- (fun id -> intros_patterns b avoid ids ((loc,id)::thin) destopt bound (n+1) tac l)
+ (fun id -> intro_patterns_core b avoid ids ((loc,id)::thin) destopt bound (n+1) tac l)
| IntroIdentifier id ->
check_thin_clash_then id thin avoid (fun thin ->
intro_then_gen (NamingMustBe (loc,id)) destopt true false
- (fun id -> intros_patterns b avoid (id::ids) thin destopt bound (n+1) tac l))
+ (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound (n+1) tac l))
| IntroAnonymous ->
intro_then_gen (NamingAvoid (avoid@explicit_intro_names l))
destopt true false
- (fun id -> intros_patterns b avoid (id::ids) thin destopt bound (n+1) tac l)
+ (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound (n+1) tac l)
| IntroFresh id ->
(* todo: avoid thinned names to interfere with generation of fresh name *)
intro_then_gen (NamingBasedOn (id, avoid@explicit_intro_names l))
destopt true false
- (fun id -> intros_patterns b avoid (id::ids) thin destopt bound (n+1) tac l)
- | IntroForthcoming onlydeps ->
- intro_forthcoming_then_gen (NamingAvoid (avoid@explicit_intro_names l))
- destopt onlydeps n bound
- (fun ids -> intros_patterns b avoid ids thin destopt bound (n+List.length ids) tac l)
+ (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound (n+1) tac l)
+
+and intro_pattern_action loc b style pat thin tac id = match pat with
| IntroOrAndPattern ll ->
- intro_then_force
- (intro_or_and_pattern loc (b || not (List.is_empty l)) ll thin
- (fun thin bound' -> intros_patterns b avoid ids thin destopt bound' 0 (fun ids thin -> intros_patterns b avoid ids thin destopt bound (n+1) tac l)))
+ intro_or_and_pattern loc b ll thin tac id
| IntroInjection l' ->
- intro_then_force
- (intro_decomp_eq loc l' thin
- (fun thin bound' -> intros_patterns b avoid ids thin destopt bound' 0 (fun ids thin -> intros_patterns b avoid ids thin destopt bound (n+1) tac l)))
+ intro_decomp_eq loc l' thin tac id
| IntroRewrite l2r ->
- intro_then_gen (NamingAvoid(avoid@explicit_intro_names l))
- MoveLast true false
- (fun id ->
- Tacticals.New.tclTHENLAST (* Skip the side conditions of the rewriting step *)
- (rewrite_hyp l2r id)
- (intros_patterns b avoid ids thin destopt bound (n+1) tac l))
+ Tacticals.New.tclTHENLAST
+ (* Skip the side conditions of the rewriting step *)
+ (rewrite_hyp style l2r id)
+ (tac thin None [])
-let intros_pattern_bound n destopt =
- intros_patterns true [] [] [] destopt
+let intro_patterns_bound_to n destopt =
+ intro_patterns_core true [] [] [] destopt
(Some (true,n)) 0 (fun _ -> clear_wildcards)
(* The following boolean governs what "intros []" do on examples such
@@ -1802,16 +1815,19 @@ let intros_pattern_bound n destopt =
*)
let bracketing_last_or_and_intro_pattern = false
-let intros_pattern destopt =
- intros_patterns bracketing_last_or_and_intro_pattern
+let intro_patterns_to destopt =
+ intro_patterns_core bracketing_last_or_and_intro_pattern
[] [] [] destopt None 0 (fun _ l -> clear_wildcards l)
-let intro_pattern destopt pat =
- intros_pattern destopt [dloc,pat]
+let intro_pattern_to destopt pat =
+ intro_patterns_to destopt [dloc,pat]
+
+let intro_patterns = intro_patterns_to MoveLast
-let intro_patterns = function
- | [] -> Tacticals.New.tclREPEAT intro
- | l -> intros_pattern MoveLast l
+(* Implements "intros" *)
+let intros_patterns = function
+ | [] -> intros
+ | l -> intro_patterns_to MoveLast l
(**************************)
(* Other cut tactics *)
@@ -1823,31 +1839,17 @@ let rec prepare_naming loc = function
| IntroFresh id -> NamingBasedOn (id,[])
| IntroWildcard ->
error "Did you really mind erasing the newly generated hypothesis?"
- | IntroRewrite _
- | IntroOrAndPattern _
- | IntroInjection _
- | IntroForthcoming _ -> assert false
let rec prepare_intros_loc loc dft = function
- | IntroIdentifier _
- | IntroAnonymous
- | IntroFresh _
- | IntroWildcard as ipat ->
+ | IntroNaming ipat ->
prepare_naming loc ipat,
(fun _ -> Proofview.tclUNIT ())
- | IntroRewrite l2r ->
- prepare_naming loc dft,
- (fun id -> Hook.get forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl)
- | IntroOrAndPattern ll ->
+ | IntroAction ipat ->
prepare_naming loc dft,
- (intro_or_and_pattern loc true ll []
- (fun thin bound -> intros_patterns true [] [] thin MoveLast bound 0
- (fun _ l -> clear_wildcards l)))
- | IntroInjection l ->
- prepare_naming loc dft,
- (intro_decomp_eq loc l []
- (fun thin bound -> intros_patterns true [] [] thin MoveLast bound 0
- (fun _ l -> clear_wildcards l)))
+ (let tac thin bound =
+ intro_patterns_core true [] [] thin MoveLast bound 0
+ (fun _ l -> clear_wildcards l) in
+ fun id -> intro_pattern_action loc true true ipat [] tac id)
| IntroForthcoming _ -> user_err_loc
(loc,"",str "Introduction pattern for one hypothesis expected.")
@@ -1857,7 +1859,7 @@ let prepare_intros dft = function
let ipat_of_name = function
| Anonymous -> None
- | Name id -> Some (dloc, IntroIdentifier id)
+ | Name id -> Some (dloc, IntroNaming (IntroIdentifier id))
let head_ident c =
let c = fst (decompose_app ((strip_lam_assum c))) in
@@ -1882,20 +1884,14 @@ let enough_tac na = assert_as false (ipat_of_name na)
(* apply in as *)
let as_tac id ipat = match ipat with
- | Some (loc,IntroRewrite l2r) ->
- Hook.get forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl
- | Some (loc,IntroOrAndPattern ll) ->
- intro_or_and_pattern loc true ll []
- (fun thin bound -> intros_patterns true [] [] thin MoveLast bound 0 (fun _ l -> clear_wildcards l))
- id
- | Some (loc,IntroInjection l) ->
- intro_decomp_eq loc l []
- (fun thin bound -> intros_patterns true [] [] thin MoveLast bound 0 (fun _ l -> clear_wildcards l))
- id
- | Some (loc,
- (IntroIdentifier _ | IntroAnonymous | IntroFresh _ |
- IntroWildcard | IntroForthcoming _)) ->
- user_err_loc (loc,"", str "Disjunctive/conjunctive pattern expected")
+ | Some (loc,IntroAction pat) ->
+ let tac thin bound =
+ intro_patterns_core true [] [] thin MoveLast bound 0
+ (fun _ l -> clear_wildcards l) in
+ intro_pattern_action loc true true pat [] tac id
+ | Some (loc, (IntroNaming _ | IntroForthcoming _)) ->
+ user_err_loc (loc,"",
+ str "Disjunctive, conjunctive or equality pattern expected")
| None -> Proofview.tclUNIT ()
let tclMAPLAST tacfun l =
@@ -2254,23 +2250,22 @@ let check_unused_names names =
++ str": " ++ prlist_with_sep spc Miscprint.pr_intro_pattern names)
let intropattern_of_name gl avoid = function
- | Anonymous -> IntroAnonymous
- | Name id -> IntroIdentifier (new_fresh_id avoid id gl)
-
+ | Anonymous -> IntroNaming IntroAnonymous
+ | Name id -> IntroNaming (IntroIdentifier (new_fresh_id avoid id gl))
let rec consume_pattern avoid na isdep gl = function
| [] -> ((dloc, intropattern_of_name gl avoid na), [])
- | (loc,IntroAnonymous)::names ->
- let avoid = avoid@explicit_intro_names names in
- ((loc,intropattern_of_name gl avoid na), names)
| (loc,IntroForthcoming true)::names when not isdep ->
consume_pattern avoid na isdep gl names
| (loc,IntroForthcoming _)::names as fullpat ->
let avoid = avoid@explicit_intro_names names in
((loc,intropattern_of_name gl avoid na), fullpat)
- | (loc,IntroFresh id')::names ->
+ | (loc,IntroNaming IntroAnonymous)::names ->
+ let avoid = avoid@explicit_intro_names names in
+ ((loc,intropattern_of_name gl avoid na), names)
+ | (loc,IntroNaming (IntroFresh id'))::names ->
let avoid = avoid@explicit_intro_names names in
- ((loc,IntroIdentifier (new_fresh_id avoid id' gl)), names)
+ ((loc,IntroNaming (IntroIdentifier (new_fresh_id avoid id' gl))), names)
| pat::names -> (pat,names)
let re_intro_dependent_hypotheses (lstatus,rstatus) (_,tophyp) =
@@ -2282,16 +2277,16 @@ let re_intro_dependent_hypotheses (lstatus,rstatus) (_,tophyp) =
(intros_move rstatus)
(intros_move newlstatus)
-let safe_dest_intros_patterns avoid thin dest pat tac =
+let safe_dest_intro_patterns avoid thin dest pat tac =
Proofview.tclORELSE
- (intros_patterns true avoid [] thin dest None 0 tac pat)
+ (intro_patterns_core true avoid [] thin dest None 0 tac pat)
begin function
| UserError ("move_hyp",_) ->
(* May happen if the lemma has dependent arguments that are resolved
only after cook_sign is called, e.g. as in "destruct dec" in context
"dec:forall x, {x=0}+{x<>0}; a:A |- if dec a then True else False"
where argument a of dec will be found only lately *)
- intros_patterns true avoid [] [] MoveLast None 0 tac pat
+ intro_patterns_core true avoid [] [] MoveLast None 0 tac pat
| e -> Proofview.tclZERO e
end
@@ -2331,17 +2326,17 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
(IndArg,depind,hyprecname) :: ra' ->
Proofview.Goal.raw_enter begin fun gl ->
let (recpat,names) = match names with
- | [loc,IntroIdentifier id as pat] ->
+ | [loc,IntroNaming (IntroIdentifier id) as pat] ->
let id' = next_ident_away (add_prefix "IH" id) avoid in
- (pat, [dloc, IntroIdentifier id'])
+ (pat, [dloc, IntroNaming (IntroIdentifier id')])
| _ -> consume_pattern avoid (Name recvarname) deprec gl names in
let dest = get_recarg_dest dests in
- safe_dest_intros_patterns avoid thin dest [recpat] (fun ids thin ->
+ safe_dest_intro_patterns avoid thin dest [recpat] (fun ids thin ->
Proofview.Goal.raw_enter begin fun gl ->
let (hyprec,names) =
consume_pattern avoid (Name hyprecname) depind gl names
in
- safe_dest_intros_patterns avoid thin MoveLast [hyprec] (fun ids' thin ->
+ safe_dest_intro_patterns avoid thin MoveLast [hyprec] (fun ids' thin ->
peel_tac ra' (update_dest dests ids') names thin)
end)
end
@@ -2350,7 +2345,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
(* Rem: does not happen in Coq schemes, only in user-defined schemes *)
let pat,names =
consume_pattern avoid (Name hyprecname) dep gl names in
- safe_dest_intros_patterns avoid thin MoveLast [pat] (fun ids thin ->
+ safe_dest_intro_patterns avoid thin MoveLast [pat] (fun ids thin ->
peel_tac ra' (update_dest dests ids) names thin)
end
| (RecArg,dep,recvarname) :: ra' ->
@@ -2358,14 +2353,14 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
let (pat,names) =
consume_pattern avoid (Name recvarname) dep gl names in
let dest = get_recarg_dest dests in
- safe_dest_intros_patterns avoid thin dest [pat] (fun ids thin ->
+ safe_dest_intro_patterns avoid thin dest [pat] (fun ids thin ->
peel_tac ra' dests names thin)
end
| (OtherArg,dep,_) :: ra' ->
Proofview.Goal.raw_enter begin fun gl ->
let (pat,names) = consume_pattern avoid Anonymous dep gl names in
let dest = get_recarg_dest dests in
- safe_dest_intros_patterns avoid thin dest [pat] (fun ids thin ->
+ safe_dest_intro_patterns avoid thin dest [pat] (fun ids thin ->
peel_tac ra' dests names thin)
end
| [] ->
@@ -3536,7 +3531,7 @@ let induction_gen clear_flag isrec with_evars elim (eqname,names) (sigma,(c,lbin
let induction_gen_l isrec with_evars elim (eqname,names) lc =
if not (Option.is_empty eqname) then
errorlabstrm "" (str "Do not know what to do with " ++
- Miscprint.pr_intro_pattern (Option.get eqname));
+ Miscprint.pr_intro_pattern_naming (snd (Option.get eqname)));
let newlc = ref [] in
let letids = ref [] in
let rec atomize_list l =
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index f50e52a19f..77e1938c68 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -102,12 +102,16 @@ val use_clear_hyp_by_default : unit -> bool
(** {6 Introduction tactics with eliminations. } *)
-val intro_pattern : Id.t move_location -> intro_pattern_expr -> unit Proofview.tactic
val intro_patterns : intro_pattern_expr located list -> unit Proofview.tactic
-val intros_pattern :
- Id.t move_location -> intro_pattern_expr located list -> unit Proofview.tactic
-val intros_pattern_bound :
- int -> Id.t move_location -> intro_pattern_expr located list -> unit Proofview.tactic
+val intro_patterns_to : Id.t move_location -> intro_pattern_expr located list ->
+ unit Proofview.tactic
+val intro_patterns_bound_to : int -> Id.t move_location ->
+ intro_pattern_expr located list -> unit Proofview.tactic
+val intro_pattern_to : Id.t move_location -> intro_pattern_expr ->
+ unit Proofview.tactic
+
+(** Implements "intros", with [] standing for "**" *)
+val intros_patterns : intro_pattern_expr located list -> unit Proofview.tactic
(** {6 Exact tactics. } *)
@@ -267,7 +271,8 @@ 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_expr located option * intro_pattern_expr located option ->
+ intro_pattern_naming_expr located option *
+ or_and_intro_pattern_expr located option ->
clause option -> unit Proofview.tactic
(** {6 Case analysis tactics. } *)
@@ -279,14 +284,16 @@ 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_expr located option * intro_pattern_expr located option ->
+ intro_pattern_naming_expr located option *
+ or_and_intro_pattern_expr located option ->
clause option -> unit Proofview.tactic
(** {6 Generic case analysis / induction tactics. } *)
val induction_destruct : rec_flag -> evars_flag ->
((evar_map * constr with_bindings) induction_arg *
- (intro_pattern_expr located option * intro_pattern_expr located option))
+ (intro_pattern_naming_expr located option *
+ or_and_intro_pattern_expr located option))
list *
constr with_bindings option *
clause option -> unit Proofview.tactic
@@ -341,9 +348,9 @@ val cut_replacing : Id.t -> types -> unit Proofview.tactic -> unit
val assert_as : bool -> intro_pattern_expr located option -> constr -> unit Proofview.tactic
val forward : bool -> unit Proofview.tactic option -> intro_pattern_expr located option -> constr -> unit Proofview.tactic
-val letin_tac : (bool * intro_pattern_expr located) option -> Name.t ->
+val letin_tac : (bool * intro_pattern_naming_expr located) option -> Name.t ->
constr -> types option -> clause -> unit Proofview.tactic
-val letin_pat_tac : (bool * intro_pattern_expr located) option -> Name.t ->
+val letin_pat_tac : (bool * intro_pattern_naming_expr located) option -> Name.t ->
evar_map * constr -> clause -> unit Proofview.tactic
val assert_tac : Name.t -> types -> unit Proofview.tactic
val enough_tac : Name.t -> types -> unit Proofview.tactic
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index c3dc8f89db..948a726b8c 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -86,9 +86,8 @@ let destruct_on_using c id =
destruct false
[None,Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))]
None
- (None,Some (dl,IntroOrAndPattern [
- [dl,IntroAnonymous];
- [dl,IntroIdentifier id]]))
+ (None,Some (dl,[[dl,IntroNaming IntroAnonymous];
+ [dl,IntroNaming (IntroIdentifier id)]]))
None
let destruct_on c =
@@ -595,9 +594,9 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
(destruct false [None,Tacexpr.ElimOnConstr
(Evd.empty,((mkVar freshz,NoBindings)))]
None
- (None, Some (dl,IntroOrAndPattern [[
- dl,IntroIdentifier fresht;
- dl,IntroIdentifier freshz]])) None)
+ (None, Some (dl,[[
+ dl,IntroNaming (IntroIdentifier fresht);
+ dl,IntroNaming (IntroIdentifier freshz)]])) None)
end
]);
(*
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 14:19:06 +0000