aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES2
-rw-r--r--doc/refman/RefMan-tac.tex117
-rw-r--r--interp/constrarg.ml2
-rw-r--r--interp/constrarg.mli2
-rw-r--r--intf/misctypes.mli14
-rw-r--r--intf/tacexpr.mli16
-rw-r--r--parsing/g_tactic.ml42
-rw-r--r--parsing/pcoq.mli2
-rw-r--r--plugins/funind/g_indfun.ml42
-rw-r--r--plugins/funind/indfun.mli2
-rw-r--r--printing/miscprint.ml18
-rw-r--r--printing/miscprint.mli6
-rw-r--r--printing/pptactic.ml51
-rw-r--r--tactics/elim.mli2
-rw-r--r--tactics/equality.mli4
-rw-r--r--tactics/inv.ml2
-rw-r--r--tactics/inv.mli6
-rw-r--r--tactics/taccoerce.mli7
-rw-r--r--tactics/tacintern.ml62
-rw-r--r--tactics/tacinterp.ml163
-rw-r--r--tactics/tacticals.ml2
-rw-r--r--tactics/tacticals.mli16
-rw-r--r--tactics/tactics.ml107
-rw-r--r--tactics/tactics.mli24
-rw-r--r--theories/Wellfounded/Lexicographic_Exponentiation.v3
25 files changed, 352 insertions, 282 deletions
diff --git a/CHANGES b/CHANGES
index be41a7724..bef29d3d1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -144,6 +144,8 @@ Tactics
- Now "appcontext" and "context" behave the same. The old buggy behaviour of
"context" can be retrieved at parse time by setting the
"Tactic Compat Context" flag. (possible source of incompatibilities).
+- New introduction pattern p/c which applies lemma c on the fly on the
+ hypothesis under consideration before continuing with introduction pattern p.
- New introduction pattern [= x1 .. xn] applies "injection as [x1 .. xn]"
on the fly if next hypothesis to introduce is an injectible equality
(idea borrowed from Georges Gonthier). Introduction pattern [=] applies
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 11568bb4d..27f8e3024 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -538,16 +538,14 @@ This works as {\tt apply \nelist{{\term} with {\bindinglist}}{,} in
{\ident}} but turns unresolved bindings into existential variables, if
any, instead of failing.
-\item {\tt apply \nelist{{\term} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}}
+\item {\tt apply \nelist{{\term} with {\bindinglist}}{,} in {\ident} as {\intropattern}}
This works as {\tt apply \nelist{{\term} with {\bindinglist}}{,} in
-{\ident}} then destructs the hypothesis {\ident} along
-{\disjconjintropattern} as {\tt destruct {\ident} as
-{\disjconjintropattern}} would.
+{\ident}} then applies the {\intropattern} to the hypothesis {\ident}.
-\item {\tt eapply \nelist{{\term} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}}
+\item {\tt eapply \nelist{{\term} with {\bindinglist}}{,} in {\ident} as {\intropattern}}
-This works as {\tt apply \nelist{{\term} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}} but using {\tt eapply}.
+This works as {\tt apply \nelist{{\term} with {\bindinglist}}{,} in {\ident} as {\intropattern}} but using {\tt eapply}.
\item {\tt simple apply {\term} in {\ident}}
\tacindex{simple apply \dots\ in}
@@ -562,8 +560,8 @@ conversion of {\tt id ?1234} and {\tt O} where {\tt ?1234} is a variable to
instantiate. Tactic {\tt simple apply {\term} in {\ident}} does not
either traverse tuples as {\tt apply {\term} in {\ident}} does.
-\item {\tt \zeroone{simple} apply \nelist{{\term} \zeroone{with {\bindinglist}}}{,} in {\ident} \zeroone{as {\disjconjintropattern}}}\\
-{\tt \zeroone{simple} eapply \nelist{{\term} \zeroone{with {\bindinglist}}}{,} in {\ident} \zeroone{as {\disjconjintropattern}}}
+\item {\tt \zeroone{simple} apply \nelist{{\term} \zeroone{with {\bindinglist}}}{,} in {\ident} \zeroone{as {\intropattern}}}\\
+{\tt \zeroone{simple} eapply \nelist{{\term} \zeroone{with {\bindinglist}}}{,} in {\ident} \zeroone{as {\intropattern}}}
This summarizes the different syntactic variants of {\tt apply {\term}
in {\ident}} and {\tt eapply {\term} in {\ident}}.
@@ -796,19 +794,30 @@ either:
\item the pattern \texttt{?\ident}
\item an identifier
\end{itemize}
-\item a {\em composite introduction pattern}, i.e. either one of:
+\item a {\em destructing introduction pattern} which itself classifies into:
\begin{itemize}
- \item a disjunction of lists of patterns:
- {\tt [$p_{11}$ \dots\ $p_{1m_1}$ | \dots\ | $p_{11}$ \dots\ $p_{nm_n}$]}
- \item a conjunction of patterns: {\tt ($p_1$ , \dots\ , $p_n$)}
- \item a pattern for decomposing an equality: {\tt [= $p_1$ \dots\ $p_n$]}
- \item a list of patterns {\tt ($p_1$ \&\ \dots\ \&\ $p_n$)}
- for sequence of right-associative binary constructs
+ \item a {\em disjunctive/conjunctive introduction pattern}, i.e. either one of:
+ \begin{itemize}
+ \item a disjunction of lists of patterns:
+ {\tt [$p_{11}$ \dots\ $p_{1m_1}$ | \dots\ | $p_{11}$ \dots\ $p_{nm_n}$]}
+ \item a conjunction of patterns: {\tt ($p_1$ , \dots\ , $p_n$)}
+ \item a list of patterns {\tt ($p_1$ \&\ \dots\ \&\ $p_n$)}
+ for sequence of right-associative binary constructs
+ \end{itemize}
+ \item an {\em equality introduction pattern}, i.e. either one of:
+ \begin{itemize}
+ \item a pattern for decomposing an equality: {\tt [= $p_1$ \dots\ $p_n$]}
+ \item the rewriting orientations: {\tt ->} or {\tt <-}
+ \end{itemize}
+ \item the on-the-fly application of a lemma: $p${\tt /{\term}}
\end{itemize}
\item the wildcard: {\tt \_}
-\item the rewriting orientations: {\tt ->} or {\tt <-}
\end{itemize}
+Introduction patterns can be combined into lists. An {\em introduction
+ pattern list} is a list of introduction patterns possibly containing
+the filling introduction patterns {\tt *} and {\tt **}.
+
Assuming a goal of type $Q \to P$ (non-dependent product), or
of type $\forall x:T,~P$ (dependent product), the behavior of
{\tt intros $p$} is defined inductively over the structure of the
@@ -843,6 +852,13 @@ introduction pattern~$p$:
of the constructor of $I$ (observe that {\tt ($p_1$, {\ldots},
$p_n$)} is an alternative notation for {\tt [$p_1$ {\ldots}
$p_n$]});
+\item introduction via {\tt ($p_1$ \& \dots\ \& $p_n$)}
+ is a shortcut for introduction via
+ {\tt ($p_1$,(\ldots,(\dots,$p_n$)\ldots))}; it expects the
+ hypothesis to be a sequence of right-associative binary inductive
+ constructors such as {\tt conj} or {\tt ex\_intro}; for instance, an
+ hypothesis with type {\tt A\verb|/\|exists x, B\verb|/\|C\verb|/\|D} can be
+ introduced via pattern {\tt (a \& x \& b \& c \& d)};
\item if the product is over an equality type, then a pattern of the
form {\tt [=$p_{1}$ \dots\ $p_n$]} applies either {\tt injection}
(see Section~\ref{injection}) or {\tt discriminate} (see
@@ -854,13 +870,16 @@ introduction pattern~$p$:
%TODO!
%if {\tt discriminate} is applicable, the list of patterns $p_{1}$
%\dots\ $p_n$ is supposed to be empty;
-\item introduction via {\tt ($p_1$ \& \dots\ \& $p_n$)}
- is a shortcut for introduction via
- {\tt ($p_1$,(\ldots,(\dots,$p_n$)\ldots))}; it expects the
- hypothesis to be a sequence of right-associative binary inductive
- constructors such as {\tt conj} or {\tt ex\_intro}; for instance, an
- hypothesis with type {\tt A\verb|/\|exists x, B\verb|/\|C\verb|/\|D} can be
- introduced via pattern {\tt (a \& x \& b \& c \& d)};
+\item introduction over {\tt ->} (respectively {\tt <-}) expects the
+ hypothesis to be an equality and the right-hand-side (respectively
+ the left-hand-side) is replaced by the left-hand-side (respectively
+ the right-hand-side) in both the conclusion and the context of the goal;
+ if moreover the term to substitute is a variable, the hypothesis is
+ removed;
+\item introduction over a pattern $p${\tt /{\term}} first applies
+ {\term} on the hypothesis to be introduced (as in {\tt apply
+ }{\term} {\tt in}), prior to the application of the introduction
+ pattern $p$;
\item introduction on the wildcard depends on whether the product is
dependent or not: in the non-dependent case, it erases the
corresponding hypothesis (i.e. it behaves as an {\tt intro} followed
@@ -868,26 +887,37 @@ introduction pattern~$p$:
case, it succeeds and erases the variable only if the wildcard is
part of a more complex list of introduction patterns that also
erases the hypotheses depending on this variable;
-\item introduction over {\tt ->} (respectively {\tt <-}) expects the
- hypothesis to be an equality and the right-hand-side (respectively
- the left-hand-side) is replaced by the left-hand-side (respectively
- the right-hand-side) in both the conclusion and the context of the goal;
- if moreover the term to substitute is a variable, the hypothesis is
- removed.
+\item introduction over {\tt *} introduces all forthcoming quantified
+ variables appearing in a row; introduction over {\tt **} introduces
+ all forthcoming quantified variables or hypotheses until the goal is
+ not any more a quantification or an implication.
+\end{itemize}
+
+Then, if $p_1$ ... $p_n$ is a list of introduction patterns possibly
+containing {\tt *} or {\tt **}, {\tt intros $p_1$ ... $p_n$}
+\begin{itemize}
+\item introduction over {\tt *} introduces all forthcoming quantified
+ variables appearing in a row;
+\item introduction over {\tt **} introduces all forthcoming quantified
+ variables or hypotheses until the goal is not any more a
+ quantification or an implication;
+\item introduction over an introduction pattern $p$ introduces the
+ forthcoming quantified variables or premisse of the goal and applies
+ the introduction pattern $p$ to it.
\end{itemize}
\Example
\begin{coq_example}
Goal forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C.
-intros A B C [a| [_ c]] f.
+intros * [a | (_,c)] f.
apply (f a).
exact c.
Qed.
\end{coq_example}
-\Rem {\tt intros $p_1~\ldots~p_n$} is not equivalent to \texttt{intros
- $p_1$;\ldots; intros $p_n$} for the following reasons:
+\Rem {\tt intros $p_1~\ldots~p_n$} is not fully equivalent to
+\texttt{intros $p_1$;\ldots; intros $p_n$} for the following reasons:
\begin{itemize}
\item A wildcard pattern never succeeds when applied isolated on a
dependent product, while it succeeds as part of a list of
@@ -1193,9 +1223,10 @@ in the list of subgoals remaining to prove.
introduction pattern (in particular, if {\intropattern} is {\ident},
the tactic behaves like \texttt{assert ({\ident} :\ {\form})}).
- If {\intropattern} is a disjunctive/conjunctive introduction
- pattern, the tactic behaves like \texttt{assert {\form}} then destructing the
- resulting hypothesis using the given introduction pattern.
+ If {\intropattern} is a disjunctive/conjunctive or an equality
+ introduction pattern, the tactic behaves like \texttt{assert
+ {\form}} followed by an application of the given introduction
+ pattern to the resulting hypothesis.
\item \texttt{assert {\form} as {\intropattern} by {\tac}}
@@ -1215,9 +1246,9 @@ in the list of subgoals remaining to prove.
exact {\term}} where \texttt{T} is the type of {\term}.
In particular, \texttt{pose proof {\term} as {\ident}} behaves as
- \texttt{assert ({\ident} := {\term})} and \texttt{pose proof {\term} as
- {\disjconjintropattern}\tacindex{pose proof}} behaves
- like \texttt{destruct {\term} as {\disjconjintropattern}}.
+ \texttt{assert ({\ident} := {\term})} and \texttt{pose proof {\term}
+ as {\intropattern}\tacindex{pose proof}} is the same as applying
+ the {\intropattern} to {\term}.
\item \texttt{enough ({\ident} :\ {\form})}\tacindex{enough}
@@ -1514,15 +1545,15 @@ syntax {\tt destruct ({\num})} (not very interesting anyway).
This behaves as {\tt destruct {\term}} but uses the names in
{\intropattern} to name the variables introduced in the context.
The {\intropattern} must have the form {\tt [} $p_{11}$ \ldots
- $p_{1n_1}$ {\tt |} {\ldots} {\tt |} $p_{m1}$ \ldots $p_{mn_m}$ {\tt
- ]} with $m$ being the number of constructors of the type of
+ $p_{1n_1}$ {\tt |} {\ldots} {\tt |} $p_{m1}$ \ldots $p_{mn_m}$
+ {\tt ]} with $m$ being the number of constructors of the type of
{\term}. Each variable introduced by {\tt destruct} in the context
of the $i^{th}$ goal gets its name from the list $p_{i1}$ \ldots
$p_{in_i}$ in order. If there are not enough names, {\tt destruct}
invents names for the remaining variables to introduce. More
- generally, the $p_{ij}$ can be any disjunctive/conjunctive
- introduction pattern (see Section~\ref{intros-pattern}). This
- provides a concise notation for nested destruction.
+ generally, the $p_{ij}$ can be any introduction pattern (see
+ Section~\ref{intros-pattern}). This provides a concise notation for
+ chaining destruction of an hypothesis.
% It is recommended to use this variant of {\tt destruct} for
% robust proof scripts.
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index aad034c05..9c1382ba1 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 : intro_pattern_expr located uniform_genarg_type =
+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 =
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 359aab0d8..b6ff3c850 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -28,7 +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 : intro_pattern_expr located 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_ident : Id.t uniform_genarg_type
diff --git a/intf/misctypes.mli b/intf/misctypes.mli
index 3d9a344ee..390711fab 100644
--- a/intf/misctypes.mli
+++ b/intf/misctypes.mli
@@ -16,20 +16,22 @@ type patvar = Id.t
(** Introduction patterns *)
-type intro_pattern_expr =
+type 'constr intro_pattern_expr =
| IntroForthcoming of bool
| IntroNaming of intro_pattern_naming_expr
- | IntroAction of intro_pattern_action_expr
+ | IntroAction of 'constr intro_pattern_action_expr
and intro_pattern_naming_expr =
| IntroWildcard
| IntroIdentifier of Id.t
| IntroFresh of Id.t
| IntroAnonymous
-and intro_pattern_action_expr =
- | IntroOrAndPattern of or_and_intro_pattern_expr
- | IntroInjection of (Loc.t * intro_pattern_expr) list
+and 'constr intro_pattern_action_expr =
+ | IntroOrAndPattern of 'constr or_and_intro_pattern_expr
+ | IntroInjection of (Loc.t * 'constr intro_pattern_expr) list
+ | IntroApplyOn of 'constr * (Loc.t * 'constr intro_pattern_expr)
| IntroRewrite of bool
-and or_and_intro_pattern_expr = (Loc.t * intro_pattern_expr) list list
+and 'constr or_and_intro_pattern_expr =
+ (Loc.t * 'constr intro_pattern_expr) list list
(** Move destination for hypothesis *)
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 2af77eb10..9b75282ca 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 * or_and_intro_pattern_expr located option
+ inversion_kind * 'id list * 'c or_and_intro_pattern_expr located option
| DepInversion of
- inversion_kind * 'c option * or_and_intro_pattern_expr located option
+ inversion_kind * 'c option * 'c or_and_intro_pattern_expr located option
| InversionUsing of 'c * 'id list
type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b
@@ -59,7 +59,7 @@ type 'id message_token =
type 'constr induction_clause =
'constr with_bindings induction_arg *
(intro_pattern_naming_expr located option (* eqn:... *)
- * or_and_intro_pattern_expr located option) (* as ... *)
+ * 'constr or_and_intro_pattern_expr located option) (* as ... *)
type ('constr,'id) induction_clause_list =
'constr induction_clause list
@@ -106,15 +106,19 @@ 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
+
(** Generic expressions for atomic tactics *)
type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
(* Basic tactics *)
- | TacIntroPattern of intro_pattern_expr located list
+ | TacIntroPattern of 'trm intro_pattern_expr located list
| TacIntroMove of Id.t option * 'nam move_location
| TacExact of 'trm
| TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
- (clear_flag * 'nam * intro_pattern_expr located option) option
+ (clear_flag * 'nam * 'trm intro_pattern_expr located option) option
| TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
| TacCase of evars_flag * 'trm with_bindings_arg
| TacFix of Id.t option * int
@@ -123,7 +127,7 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
| TacMutualCofix of Id.t * (Id.t * 'trm) list
| TacAssert of
bool * ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr option *
- intro_pattern_expr located option * 'trm
+ 'trm intro_pattern_expr located option * 'trm
| TacGeneralize of ('trm with_occurrences * Name.t) list
| TacGeneralizeDep of 'trm
| TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag *
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 9cf476a5e..ae4bf8a12 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -307,6 +307,8 @@ GEXTEND Gram
simple_intropattern:
[ [ pat = or_and_intropattern -> !@loc, IntroAction (IntroOrAndPattern pat)
| pat = equality_intropattern -> !@loc, IntroAction pat
+ | pat = simple_intropattern; "/"; c = constr ->
+ !@loc, IntroAction (IntroApplyOn (c,pat))
| pat = naming_intropattern -> !@loc, IntroNaming pat ] ]
;
simple_binding:
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 54fcb12b0..5c0a48dd6 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -218,7 +218,7 @@ module Tactic :
val int_or_var : int or_var Gram.entry
val red_expr : raw_red_expr Gram.entry
val simple_tactic : raw_tactic_expr Gram.entry
- val simple_intropattern : intro_pattern_expr located Gram.entry
+ val simple_intropattern : constr_expr intro_pattern_expr located Gram.entry
val clause_dft_concl : Names.Id.t Loc.located Locus.clause_expr Gram.entry
val tactic_arg : raw_tactic_arg Gram.entry
val tactic_expr : raw_tactic_expr Gram.entry
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 1d63fe01a..e688204a4 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -80,7 +80,7 @@ END
let pr_intro_as_pat prc _ _ pat =
match pat with
| Some pat ->
- spc () ++ str "as" ++ spc () ++ Miscprint.pr_intro_pattern pat
+ spc () ++ str "as" ++ spc () ++ Miscprint.pr_intro_pattern prc pat
| None -> mt ()
let out_disjunctive = function
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index f88a72ff5..34985f2c4 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 ->
- or_and_intro_pattern_expr Loc.located option ->
+ Term.constr or_and_intro_pattern_expr Loc.located option ->
Proof_type.goal Tacmach.sigma -> Proof_type.goal list Evd.sigma
diff --git a/printing/miscprint.ml b/printing/miscprint.ml
index 3193a74a0..682cc3abe 100644
--- a/printing/miscprint.ml
+++ b/printing/miscprint.ml
@@ -11,11 +11,11 @@ open Pp
(** Printing of [intro_pattern] *)
-let rec pr_intro_pattern (_,pat) = match pat with
+let rec pr_intro_pattern prc (_,pat) = match pat with
| IntroForthcoming true -> str "*"
| IntroForthcoming false -> str "**"
| IntroNaming p -> pr_intro_pattern_naming p
- | IntroAction p -> pr_intro_pattern_action p
+ | IntroAction p -> pr_intro_pattern_action prc p
and pr_intro_pattern_naming = function
| IntroWildcard -> str "_"
@@ -23,19 +23,21 @@ and pr_intro_pattern_naming = function
| IntroFresh id -> str "?" ++ Nameops.pr_id id
| IntroAnonymous -> str "?"
-and pr_intro_pattern_action = function
- | IntroOrAndPattern pll -> pr_or_and_intro_pattern pll
+and pr_intro_pattern_action prc = function
+ | IntroOrAndPattern pll -> pr_or_and_intro_pattern prc pll
| IntroInjection pl ->
- str "[=" ++ hv 0 (prlist_with_sep spc pr_intro_pattern pl) ++ str "]"
+ str "[=" ++ hv 0 (prlist_with_sep spc (pr_intro_pattern prc) pl) ++
+ str "]"
+ | IntroApplyOn (c,pat) -> pr_intro_pattern prc pat ++ str "/" ++ prc c
| IntroRewrite true -> str "->"
| IntroRewrite false -> str "<-"
-and pr_or_and_intro_pattern = function
+and pr_or_and_intro_pattern prc = function
| [pl] ->
- str "(" ++ hv 0 (prlist_with_sep pr_comma pr_intro_pattern pl) ++ str ")"
+ str "(" ++ hv 0 (prlist_with_sep pr_comma (pr_intro_pattern prc) pl) ++ str ")"
| pll ->
str "[" ++
- hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
+ hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc (pr_intro_pattern prc)) pll)
++ str "]"
(** Printing of [move_location] *)
diff --git a/printing/miscprint.mli b/printing/miscprint.mli
index d242bad3a..583c174c4 100644
--- a/printing/miscprint.mli
+++ b/printing/miscprint.mli
@@ -10,9 +10,11 @@ open Misctypes
(** Printing of [intro_pattern] *)
-val pr_intro_pattern : intro_pattern_expr Loc.located -> Pp.std_ppcmds
+val pr_intro_pattern :
+ ('a -> Pp.std_ppcmds) -> 'a intro_pattern_expr Loc.located -> Pp.std_ppcmds
-val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds
+val pr_or_and_intro_pattern :
+ ('a -> Pp.std_ppcmds) -> 'a or_and_intro_pattern_expr -> Pp.std_ppcmds
val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.std_ppcmds
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 3caee02de..5ea4293c9 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -347,23 +347,28 @@ 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_disjunctive_ipat (_,ipatl) =
- str "as " ++ Miscprint.pr_or_and_intro_pattern ipatl
+let pr_as_disjunctive_ipat prc (_,ipatl) =
+ str "as " ++ Miscprint.pr_or_and_intro_pattern prc 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
+let pr_with_induction_names prc = function
| None, None -> mt ()
| Some eqpat, None -> spc () ++ hov 1 (pr_eqn_ipat eqpat)
- | None, Some ipat -> spc () ++ hov 1 (pr_as_disjunctive_ipat ipat)
+ | None, Some ipat -> spc () ++ hov 1 (pr_as_disjunctive_ipat prc ipat)
| Some eqpat, Some ipat ->
- spc () ++ hov 1 (pr_as_disjunctive_ipat ipat ++ spc () ++ pr_eqn_ipat eqpat)
+ spc () ++
+ hov 1 (pr_as_disjunctive_ipat prc ipat ++ spc () ++ pr_eqn_ipat eqpat)
+
+let pr_as_intro_pattern prc ipat =
+ spc () ++ hov 1 (str "as" ++ spc () ++ Miscprint.pr_intro_pattern prc ipat)
-let pr_with_inversion_names = function
+let pr_with_inversion_names prc = function
| None -> mt ()
- | Some ipat -> pr_as_disjunctive_ipat ipat
+ | Some ipat -> pr_as_disjunctive_ipat prc ipat
+
+let pr_as_ipat prc = function
+ | None -> mt ()
+ | Some ipat -> pr_as_intro_pattern prc ipat
let pr_as_name = function
| Anonymous -> mt ()
@@ -382,7 +387,7 @@ let pr_assertion prc _prlc ipat c = match ipat with
spc() ++ surround (pr_intro_pattern ipat ++ str " :" ++ spc() ++ prlc c)
*)
| ipat ->
- spc() ++ prc c ++ pr_as_ipat ipat
+ spc() ++ prc c ++ pr_as_ipat prc ipat
let pr_assumption prc prlc ipat c = match ipat with
(* Use this "optimisation" or use only the general case ?*)
@@ -390,7 +395,7 @@ let pr_assumption prc prlc ipat c = match ipat with
| Some (_,IntroNaming (IntroIdentifier id)) ->
spc() ++ surround (pr_id id ++ str " :" ++ spc() ++ prlc c)
| ipat ->
- spc() ++ prc c ++ pr_as_ipat ipat
+ spc() ++ prc c ++ pr_as_ipat prc ipat
let pr_by_tactic prt = function
| TacId [] -> mt ()
@@ -411,10 +416,10 @@ let pr_simple_hyp_clause pr_id = function
| [] -> mt ()
| l -> pr_in (spc () ++ prlist_with_sep spc pr_id l)
-let pr_in_hyp_as pr_id = function
+let pr_in_hyp_as prc pr_id = function
| None -> mt ()
| Some (clear,id,ipat) ->
- pr_in (spc () ++ pr_clear_flag clear pr_id id) ++ pr_as_ipat ipat
+ pr_in (spc () ++ pr_clear_flag clear pr_id id) ++ pr_as_ipat prc ipat
let pr_clauses default_is_concl pr_id = function
| { onhyps=Some []; concl_occs=occs }
@@ -655,7 +660,7 @@ and pr_atom1 = function
| TacIntroPattern [] as t -> pr_atom0 t
| TacIntroPattern (_::_ as p) ->
hov 1 (str "intros" ++ spc () ++
- prlist_with_sep spc Miscprint.pr_intro_pattern p)
+ prlist_with_sep spc (Miscprint.pr_intro_pattern pr_constr) p)
| TacIntroMove (None,MoveLast) as t -> pr_atom0 t
| TacIntroMove (Some id,MoveLast) -> str "intro " ++ pr_id id
| TacIntroMove (ido,hto) ->
@@ -666,7 +671,7 @@ and pr_atom1 = function
hov 1 ((if a then mt() else str "simple ") ++
str (with_evars ev "apply") ++ spc () ++
prlist_with_sep pr_comma pr_with_bindings_arg cb ++
- pr_in_hyp_as pr_ident inhyp)
+ pr_in_hyp_as pr_constr pr_ident inhyp)
| TacElim (ev,cb,cbo) ->
hov 1 (str (with_evars ev "elim") ++ pr_arg pr_with_bindings_arg cb ++
pr_opt pr_eliminator cbo)
@@ -719,7 +724,7 @@ and pr_atom1 = function
spc () ++
prlist_with_sep pr_comma (fun ((clear_flag,h),ids) ->
pr_clear_flag clear_flag (pr_induction_arg pr_constr pr_lconstr) h ++
- pr_with_induction_names ids) l ++
+ pr_with_induction_names pr_constr ids) l ++
pr_opt pr_eliminator el ++
pr_opt_no_spc (pr_clauses None pr_ident) cl)
| TacDoubleInduction (h1,h2) ->
@@ -795,11 +800,11 @@ and pr_atom1 = function
| TacInversion (DepInversion (k,c,ids),hyp) ->
hov 1 (str "dependent " ++ pr_induction_kind k ++ spc () ++
pr_quantified_hypothesis hyp ++
- pr_with_inversion_names ids ++ pr_with_constr pr_constr c)
+ pr_with_inversion_names pr_constr ids ++ pr_with_constr pr_constr c)
| TacInversion (NonDepInversion (k,cl,ids),hyp) ->
hov 1 (pr_induction_kind k ++ spc () ++
pr_quantified_hypothesis hyp ++
- pr_with_inversion_names ids ++ pr_simple_hyp_clause pr_ident cl)
+ pr_with_inversion_names pr_constr ids ++ pr_simple_hyp_clause pr_ident cl)
| TacInversion (InversionUsing (c,cl),hyp) ->
hov 1 (str "inversion" ++ spc() ++ pr_quantified_hypothesis hyp ++
spc () ++ str "using" ++ spc () ++ pr_constr c ++
@@ -1017,12 +1022,12 @@ let () =
pr_reference (pr_or_var (pr_located pr_global)) pr_global;
Genprint.register_print0
Constrarg.wit_intro_pattern
- Miscprint.pr_intro_pattern
- Miscprint.pr_intro_pattern
- Miscprint.pr_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);
Genprint.register_print0
Constrarg.wit_clause_dft_concl
- (pr_clauses (Some true) (pr_lident))
+ (pr_clauses (Some true) pr_lident)
(pr_clauses (Some true) pr_lident)
(pr_clauses (Some true) (fun id -> pr_lident (Loc.ghost,id)))
;
diff --git a/tactics/elim.mli b/tactics/elim.mli
index b5e89de08..df75f8ba5 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -14,7 +14,7 @@ open Misctypes
(** Eliminations tactics. *)
val introCaseAssumsThen :
- (intro_pattern_expr Loc.located list -> branch_assumptions -> unit Proofview.tactic) ->
+ (Tacexpr.intro_patterns -> branch_assumptions -> unit Proofview.tactic) ->
branch_args -> unit Proofview.tactic
val h_decompose : inductive list -> constr -> unit Proofview.tactic
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 4899cd91d..9008af77b 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -77,9 +77,9 @@ val discrHyp : Id.t -> unit Proofview.tactic
val discrEverywhere : evars_flag -> unit Proofview.tactic
val discr_tac : evars_flag ->
constr with_bindings induction_arg option -> unit Proofview.tactic
-val inj : intro_pattern_expr Loc.located list option -> evars_flag ->
+val inj : intro_patterns option -> evars_flag ->
clear_flag -> constr with_bindings -> unit Proofview.tactic
-val injClause : intro_pattern_expr Loc.located list option -> evars_flag ->
+val injClause : intro_patterns option -> evars_flag ->
constr with_bindings induction_arg option -> unit Proofview.tactic
val injHyp : clear_flag -> Id.t -> unit Proofview.tactic
val injConcl : unit Proofview.tactic
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 089fef4bc..49a5bcd7e 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -396,6 +396,8 @@ let rec get_names allow_conj (loc,pat) = match pat with
error "Injection patterns not allowed for inversion equations."
| IntroAction (IntroOrAndPattern l) ->
error "Disjunctive patterns not allowed for inversion equations."
+ | IntroAction (IntroApplyOn (c,pat)) ->
+ error "Apply patterns not allowed for inversion equations."
| IntroNaming (IntroIdentifier id) ->
(Some id,[id])
diff --git a/tactics/inv.mli b/tactics/inv.mli
index 7416d29bb..a71b5eeb3 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 -> or_and_intro_pattern_expr located option -> Id.t list ->
+ inversion_kind -> constr or_and_intro_pattern_expr located option -> Id.t list ->
quantified_hypothesis -> unit Proofview.tactic
-val inv : inversion_kind -> or_and_intro_pattern_expr located option ->
+val inv : inversion_kind -> constr or_and_intro_pattern_expr located option ->
quantified_hypothesis -> unit Proofview.tactic
val dinv : inversion_kind -> constr option ->
- or_and_intro_pattern_expr located option -> quantified_hypothesis -> unit Proofview.tactic
+ constr 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.mli b/tactics/taccoerce.mli
index f2b3b225b..629a218e5 100644
--- a/tactics/taccoerce.mli
+++ b/tactics/taccoerce.mli
@@ -50,7 +50,10 @@ 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 -> intro_pattern_expr
+val coerce_to_intro_pattern : Environ.env -> Value.t -> constr intro_pattern_expr
+
+val coerce_to_intro_pattern_naming :
+ Environ.env -> Value.t -> intro_pattern_naming_expr
val coerce_to_intro_pattern_naming :
Environ.env -> Value.t -> intro_pattern_naming_expr
@@ -71,7 +74,7 @@ val coerce_to_evaluable_ref :
val coerce_to_constr_list : Environ.env -> Value.t -> constr list
val coerce_to_intro_pattern_list :
- Loc.t -> Environ.env -> Value.t -> intro_pattern_expr Loc.located list
+ Loc.t -> Environ.env -> Value.t -> Tacexpr.intro_patterns
val coerce_to_hyp : Environ.env -> Value.t -> Id.t
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 0d086d842..cf8cda014 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -215,36 +215,6 @@ 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, 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 ->
@@ -287,6 +257,38 @@ let intern_constr_with_bindings ist (c,bl) =
let intern_constr_with_bindings_arg ist (clear,c) =
(clear,intern_constr_with_bindings ist c)
+let rec intern_intro_pattern lf ist = function
+ | 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
+ | IntroApplyOn (c,pat) ->
+ IntroApplyOn (intern_constr ist c, intern_intro_pattern lf ist pat)
+
+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)
+
(* TODO: catch ltac vars *)
let intern_induction_arg ist = function
| clear,ElimOnConstr c -> clear,ElimOnConstr (intern_constr_with_bindings ist c)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index d9963a615..026ed94a4 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -425,6 +425,7 @@ let rec intropattern_ids (loc,pat) = match pat with
List.flatten (List.map intropattern_ids (List.flatten ll))
| IntroAction (IntroInjection l) ->
List.flatten (List.map intropattern_ids l)
+ | IntroAction (IntroApplyOn (c,pat)) -> intropattern_ids pat
| IntroNaming (IntroWildcard | IntroAnonymous | IntroFresh _)
| IntroAction (IntroRewrite _)
| IntroForthcoming _ -> []
@@ -724,7 +725,7 @@ 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 (out_gen (topwit wit_intro_pattern) v)
+ Miscprint.pr_intro_pattern (pr_constr_env env) (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
@@ -752,49 +753,69 @@ let interp_message ist gl l =
are raised now and not at printing time *)
prlist_with_sep spc (interp_message_token ist gl) l
-let rec interp_intro_pattern ist env = function
+let rec interp_intro_pattern ist env sigma = function
| loc, IntroAction pat ->
- loc, IntroAction (interp_intro_pattern_action ist env pat)
+ let (sigma,pat) = interp_intro_pattern_action ist env sigma pat in
+ sigma, (loc, IntroAction pat)
| loc, IntroNaming (IntroIdentifier id) ->
- loc, interp_intro_pattern_var loc ist env id
+ sigma, (loc, interp_intro_pattern_var loc ist env id)
| loc, IntroNaming pat ->
- loc, IntroNaming (snd (interp_intro_pattern_naming ist env (loc,pat)))
- | loc, IntroForthcoming _ as x -> x
+ sigma, (loc, IntroNaming (interp_intro_pattern_naming loc ist env pat))
+ | loc, IntroForthcoming _ as x -> sigma, 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_naming loc ist env = function
+ | IntroFresh id -> IntroFresh (interp_fresh_ident ist env id)
+ | IntroIdentifier id -> interp_intro_pattern_naming_var loc ist env id
+ | (IntroWildcard | IntroAnonymous) as x -> x
-and interp_intro_pattern_action ist env = function
+and interp_intro_pattern_action ist env sigma = function
| IntroOrAndPattern l ->
- IntroOrAndPattern (interp_or_and_intro_pattern ist env l)
+ let (sigma,l) = interp_or_and_intro_pattern ist env sigma l in
+ sigma, IntroOrAndPattern 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
+ 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 sigma,ipat = interp_intro_pattern ist env sigma ipat in
+ sigma, IntroApplyOn (c,ipat)
+ | IntroRewrite _ as x -> sigma, x
+
+and interp_or_and_intro_pattern ist env sigma =
+ List.fold_map (interp_intro_pattern_list_as_list ist env) sigma
+
+and interp_intro_pattern_list_as_list ist env sigma = function
| [loc,IntroNaming (IntroIdentifier id)] as l ->
- (try coerce_to_intro_pattern_list loc env (Id.Map.find id ist.lfun)
+ (try sigma, 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)
+ List.fold_map (interp_intro_pattern ist env) sigma l)
+ | l -> List.fold_map (interp_intro_pattern ist env) sigma l
+
+let interp_intro_pattern_naming_option ist env = function
+ | None -> None
+ | Some (loc,pat) -> Some (loc, interp_intro_pattern_naming loc ist env pat)
+
+let interp_or_and_intro_pattern_option ist env sigma = function
+ | None -> sigma, None
+ | Some (loc,l) ->
+ let sigma, 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) -> sigma, l
+ | _ ->
+ raise (CannotCoerceTo "a disjunctive/conjunctive introduction pattern"))
+ | l -> interp_or_and_intro_pattern ist env sigma l in
+ sigma, Some (loc,l)
+
+let interp_intro_pattern_option ist env sigma = function
+ | None -> sigma, None
+ | Some ipat ->
+ let sigma, ipat = interp_intro_pattern ist env sigma ipat in
+ sigma, Some ipat
+
+let interp_in_hyp_as ist env sigma (clear,id,ipat) =
+ let sigma, ipat = interp_intro_pattern_option ist env sigma ipat in
+ sigma,(clear,interp_hyp ist env id,ipat)
let interp_quantified_hypothesis ist = function
| AnonHyp n -> AnonHyp n
@@ -1691,8 +1712,9 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacIntroPattern l ->
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.intros_patterns patterns
+ let sigma = Proofview.Goal.sigma gl in
+ let sigma,l' = interp_intro_pattern_list_as_list ist env sigma l in
+ Tacticals.New.tclWITHHOLES false Tactics.intros_patterns sigma l'
end
| TacIntroMove (ido,hto) ->
Proofview.Goal.raw_enter begin fun gl ->
@@ -1715,15 +1737,11 @@ and interp_atomic ist tac : unit Proofview.tactic =
let sigma, l =
List.fold_map (interp_open_constr_with_bindings_arg_loc ist env) sigma cb
in
- let tac = match cl with
- | None -> fun l -> Tactics.apply_with_bindings_gen a ev l
+ let sigma,tac = match cl with
+ | None -> sigma, fun l -> Tactics.apply_with_bindings_gen a ev l
| Some cl ->
- (fun l ->
- Proofview.Goal.raw_enter begin fun gl ->
- let env = Proofview.Goal.env gl in
- let (clear,id,cl) = interp_in_hyp_as ist env cl in
- Tactics.apply_in a ev clear id l cl
- end) in
+ let sigma,(clear,id,cl) = interp_in_hyp_as ist env sigma cl in
+ sigma, fun l -> Tactics.apply_in a ev clear id l cl in
Tacticals.New.tclWITHHOLES ev tac sigma l
end
| TacElim (ev,(keep,cb),cbo) ->
@@ -1786,11 +1804,9 @@ and interp_atomic ist tac : unit Proofview.tactic =
let (sigma,c) =
(if Option.is_empty t then interp_constr else interp_type) ist env sigma c
in
- let patt = interp_intro_pattern ist env in
- Tacticals.New.tclTHEN
- (Proofview.V82.tclEVARS sigma)
- (Tactics.forward b (Option.map (interp_tactic ist) t)
- (Option.map patt ipat) c)
+ let sigma, ipat = interp_intro_pattern_option ist env sigma ipat in
+ let tac = Option.map (interp_tactic ist) t in
+ Tacticals.New.tclWITHHOLES false (Tactics.forward b tac ipat) sigma c
end
| TacGeneralize cl ->
let tac arg = Proofview.V82.tactic (Tactics.Simple.generalize_gen arg) in
@@ -1809,7 +1825,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_naming ist env) eqpat in
+ let eqpat = interp_intro_pattern_naming_option ist env eqpat in
if Locusops.is_nowhere clp then
(* We try to fully-typecheck the term *)
let (sigma,c_interp) =
@@ -1820,9 +1836,9 @@ and interp_atomic ist tac : unit Proofview.tactic =
let with_eq = if b then None else Some (true,id) in
Tactics.letin_tac with_eq na c None cl
in
- Tacticals.New.tclTHEN
- (Proofview.V82.tclEVARS sigma)
- (let_tac b (interp_fresh_name ist env na) c_interp clp eqpat)
+ Tacticals.New.tclWITHHOLES false
+ (let_tac b (interp_fresh_name ist env na) c_interp clp)
+ sigma eqpat
else
(* We try to keep the pattern structure as much as possible *)
let let_pat_tac b na c cl eqpat =
@@ -1830,8 +1846,9 @@ and interp_atomic ist tac : unit Proofview.tactic =
let with_eq = if b then None else Some (true,id) in
Tactics.letin_pat_tac with_eq na c cl
in
- let_pat_tac b (interp_fresh_name ist env na)
- (interp_pure_open_constr ist env sigma c) clp eqpat
+ Tacticals.New.tclWITHHOLES false
+ (let_pat_tac b (interp_fresh_name ist env na)
+ (interp_pure_open_constr ist env sigma c) clp) sigma eqpat
end
(* Automation tactics *)
@@ -1859,17 +1876,16 @@ and interp_atomic ist tac : unit Proofview.tactic =
Proofview.V82.nf_evar_goals <*>
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
- let l =
- List.map begin fun (c,(ipato,ipats)) ->
+ let sigma = Proofview.Goal.sigma gl in
+ let sigma,l =
+ List.fold_map begin fun sigma (c,(ipato,ipats)) ->
+ (* TODO: move sigma as a side-effect *)
let c = Tacmach.New.of_old (fun gl -> interp_induction_arg ist gl c) gl 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_pattern1 ipato,
- Option.map interp_intro_pattern2 ipats)
- end l
+ let ipato = interp_intro_pattern_naming_option ist env ipato in
+ let sigma,ipats = interp_or_and_intro_pattern_option ist env sigma ipats in
+ sigma,(c,(ipato,ipats))
+ end sigma l
in
- let sigma = Proofview.Goal.sigma gl in
let sigma,el =
Option.fold_map (interp_constr_with_bindings ist env) sigma el in
let interp_clause = interp_clause ist env in
@@ -2004,22 +2020,19 @@ and interp_atomic ist tac : unit Proofview.tactic =
in
sigma , Some c_interp
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)
- dqhyps
+ let sigma,ids = interp_or_and_intro_pattern_option ist env sigma ids in
+ Tacticals.New.tclWITHHOLES false (Inv.dinv k c_interp ids) sigma dqhyps
end
| 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_or_and_intro_pattern_loc ist env in
+ let sigma = Proofview.Goal.sigma gl 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
- (Option.map interp_intro_pattern ids)
- hyps
- dqhyps
+ let sigma, ids = interp_or_and_intro_pattern_option ist env sigma ids in
+ Tacticals.New.tclWITHHOLES false (Inv.inv_clause k ids hyps)
+ sigma dqhyps
end
| TacInversion (InversionUsing (c,idl),hyp) ->
Proofview.Goal.raw_enter begin fun gl ->
@@ -2118,7 +2131,7 @@ let () =
let () =
let interp ist gl ref = (project gl, interp_reference ist (pf_env gl) ref) in
Geninterp.register_interp0 wit_ref interp;
- let interp ist gl pat = (project gl, interp_intro_pattern ist (pf_env gl) pat) in
+ let interp ist gl pat = interp_intro_pattern ist (pf_env gl) (project gl) pat in
Geninterp.register_interp0 wit_intro_pattern interp;
let interp ist gl pat = (project gl, interp_clause ist (pf_env gl) pat) in
Geninterp.register_interp0 wit_clause_dft_concl interp;
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 8260da9d7..840cd0c05 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 : intro_pattern_expr Loc.located list}
+ branchnames : constr intro_pattern_expr Loc.located list}
type branch_assumptions = {
ba : branch_args; (* the branch args *)
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index ebe1667f2..de2bbbfae 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -108,7 +108,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 : intro_pattern_expr located list}
+ branchnames : intro_patterns}
type branch_assumptions = {
ba : branch_args; (** the branch args *)
@@ -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 -> or_and_intro_pattern_expr -> int -> unit
+ Loc.t -> constr or_and_intro_pattern_expr -> int -> unit
(** Tolerate "[]" to mean a disjunctive pattern of any length *)
-val fix_empty_or_and_pattern : int -> or_and_intro_pattern_expr ->
- or_and_intro_pattern_expr
+val fix_empty_or_and_pattern : int -> constr or_and_intro_pattern_expr ->
+ constr or_and_intro_pattern_expr
(** Useful for [as intro_pattern] modifier *)
val compute_induction_names :
- int -> or_and_intro_pattern_expr located option ->
- intro_pattern_expr located list array
+ int -> constr or_and_intro_pattern_expr located 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 :
- or_and_intro_pattern_expr located option -> (branch_args -> unit Proofview.tactic) ->
+ constr 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 :
- or_and_intro_pattern_expr located option -> (branch_args -> unit Proofview.tactic) ->
+ constr 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 4ed8b5114..44043364d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -821,7 +821,7 @@ let make_naming id t = function
[Ti] and the first one (resp last one) being [G] whose hypothesis
[id] is replaced by P using the proof given by [tac] *)
-let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) naming id clenv0 =
+let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) naming id clenv0 tac =
let clenv = Clenvtac.clenv_pose_dependent_evars with_evars clenv0 in
let clenv =
if with_classes then
@@ -839,10 +839,10 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) nami
(Proofview.V82.tclEVARS clenv.evd)
(if sidecond_first then
Tacticals.New.tclTHENFIRST
- (assert_before_gen with_clear naming new_hyp_typ) exact_tac
+ (assert_before_then_gen with_clear naming new_hyp_typ tac) exact_tac
else
Tacticals.New.tclTHENLAST
- (assert_after_gen with_clear naming new_hyp_typ) exact_tac)
+ (assert_after_then_gen with_clear naming new_hyp_typ tac) exact_tac)
(********************************************)
(* Elimination tactics *)
@@ -1083,6 +1083,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id rename i (
errorlabstrm "general_rewrite_in"
(str "Nothing to rewrite in " ++ pr_id id ++ str".");
clenv_refine_in with_evars None id elimclause''
+ (fun id -> Proofview.tclUNIT ())
end
let general_elim_clause with_evars flags id c e =
@@ -1325,7 +1326,7 @@ let apply_in_once_main flags innerclause env sigma (d,lbind) =
aux (make_clenv_binding env sigma (d,thm) lbind)
let apply_in_once sidecond_first with_delta with_destruct with_evars naming
- id (clear_flag,(loc,(d,lbind))) =
+ id (clear_flag,(loc,(d,lbind))) tac =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
@@ -1338,9 +1339,11 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
let sigma = Proofview.Goal.sigma gl in
try
let clause = apply_in_once_main flags innerclause env sigma (c,lbind) in
- Tacticals.New.tclTHEN
- (clenv_refine_in ~sidecond_first with_evars naming id clause)
- (apply_clear_request clear_flag false c)
+ clenv_refine_in ~sidecond_first with_evars naming id clause
+ (fun id ->
+ Tacticals.New.tclTHEN
+ (apply_clear_request clear_flag false c)
+ (tac id))
with e when with_destruct ->
let e = Errors.push e in
descend_in_conjunctions aux (fun _ -> raise e) c
@@ -1695,6 +1698,17 @@ let rewrite_hyp assert_style l2r id =
Tacticals.New.tclZEROMSG (str"Cannot find a known equation.")
end
+let rec prepare_naming loc = function
+ | IntroIdentifier id -> NamingMustBe (loc,id)
+ | IntroAnonymous -> NamingAvoid []
+ | IntroFresh id -> NamingBasedOn (id,[])
+ | IntroWildcard ->
+ error "Did you really mind erasing the newly generated hypothesis?"
+
+let do_replace id = function
+ | NamingMustBe (_,id') when Option.equal Id.equal id (Some id') -> true
+ | _ -> false
+
let rec explicit_intro_names = function
| (_, IntroForthcoming _) :: l -> explicit_intro_names l
| (_, IntroNaming (IntroIdentifier id)) :: l -> id :: explicit_intro_names l
@@ -1702,6 +1716,8 @@ let rec explicit_intro_names = function
List.flatten (List.map (fun l -> explicit_intro_names (l@l')) ll)
| (_, IntroAction (IntroInjection l)) :: l' ->
explicit_intro_names (l@l')
+| (_, IntroAction (IntroApplyOn (c,pat))) :: l' ->
+ explicit_intro_names (pat::l')
| (_, (IntroNaming (IntroWildcard | IntroAnonymous | IntroFresh _)
| IntroAction (IntroRewrite _))) :: l ->
explicit_intro_names l
@@ -1789,6 +1805,27 @@ 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)) ->
+ 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 [])
+
+and prepare_intros_loc loc dft = function
+ | IntroNaming ipat ->
+ prepare_naming loc ipat,
+ (fun _ -> Proofview.tclUNIT ())
+ | IntroAction ipat ->
+ prepare_naming loc dft,
+ (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.")
let intro_patterns_bound_to n destopt =
intro_patterns_core true [] [] [] destopt
@@ -1819,26 +1856,6 @@ let intros_patterns = function
(* Forward reasoning *)
(**************************)
-let rec prepare_naming loc = function
- | IntroIdentifier id -> NamingMustBe (loc,id)
- | IntroAnonymous -> NamingAvoid []
- | IntroFresh id -> NamingBasedOn (id,[])
- | IntroWildcard ->
- error "Did you really mind erasing the newly generated hypothesis?"
-
-let rec prepare_intros_loc loc dft = function
- | IntroNaming ipat ->
- prepare_naming loc ipat,
- (fun _ -> Proofview.tclUNIT ())
- | IntroAction ipat ->
- prepare_naming loc dft,
- (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.")
-
let prepare_intros dft = function
| None -> prepare_naming dloc dft, (fun _id -> Proofview.tclUNIT ())
| Some (loc,ipat) -> prepare_intros_loc loc dft ipat
@@ -1851,10 +1868,6 @@ let ipat_of_name = function
let c = fst (decompose_app ((strip_lam_assum c))) in
if isVar c then Some (destVar c) else None
-let do_replace id = function
- | NamingMustBe (_,id') when Option.equal Id.equal id (Some id') -> true
- | _ -> false
-
let assert_as first ipat c =
let naming,tac = prepare_intros IntroAnonymous ipat in
let repl = do_replace (head_ident c) naming in
@@ -1863,39 +1876,27 @@ let assert_as first ipat c =
(* apply in as *)
-let as_tac id ipat = match ipat with
- | 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 =
- List.fold_right (fun x -> Tacticals.New.tclTHENLAST (tacfun x)) l (Proofview.tclUNIT())
-
-let tclMAPFIRST tacfun l =
- List.fold_right (fun x -> Tacticals.New.tclTHENFIRST (tacfun x)) l (Proofview.tclUNIT())
-
let general_apply_in sidecond_first with_delta with_destruct with_evars
with_clear id lemmas ipat =
- let tac (naming,lemma) =
+ let tac (naming,lemma) tac id =
apply_in_once sidecond_first with_delta with_destruct with_evars
- naming id lemma in
+ naming id lemma tac in
let naming,ipat_tac = prepare_intros (IntroIdentifier id) ipat in
let clear = do_replace (Some id) naming in
- let lemmas_target =
+ let lemmas_target, last_lemma_target =
let last,first = List.sep_last lemmas in
- List.map (fun lem -> (None,lem)) first @ [(Some (clear,naming),last)]
+ List.map (fun lem -> (None,lem)) first, (Some (clear,naming),last)
in
+ (* We chain apply_in_once, ending with an intro pattern *)
+ List.fold_right tac lemmas_target (tac last_lemma_target ipat_tac) id
+
+(*
if sidecond_first then
(* Skip the side conditions of the applied lemma *)
Tacticals.New.tclTHENLAST (tclMAPLAST tac lemmas_target) (ipat_tac id)
else
Tacticals.New.tclTHENFIRST (tclMAPFIRST tac lemmas_target) (ipat_tac id)
+*)
let apply_in simple with_evars clear_flag id lemmas ipat =
general_apply_in false simple simple with_evars clear_flag id lemmas ipat
@@ -2227,7 +2228,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 names)
+ ++ str": " ++ prlist_with_sep spc (Miscprint.pr_intro_pattern Printer.pr_constr) names)
let intropattern_of_name gl avoid = function
| Anonymous -> IntroNaming IntroAnonymous
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index b974f341f..cee781a8b 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -102,16 +102,16 @@ val use_clear_hyp_by_default : unit -> bool
(** {6 Introduction tactics with eliminations. } *)
-val intro_patterns : intro_pattern_expr located list -> unit Proofview.tactic
-val intro_patterns_to : Id.t move_location -> intro_pattern_expr located list ->
+val intro_patterns : intro_patterns -> unit Proofview.tactic
+val intro_patterns_to : Id.t move_location -> intro_patterns ->
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 ->
+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 ->
unit Proofview.tactic
(** Implements user-level "intros", with [] standing for "**" *)
-val intros_patterns : intro_pattern_expr located list -> unit Proofview.tactic
+val intros_patterns : intro_patterns -> unit Proofview.tactic
(** {6 Exact tactics. } *)
@@ -193,7 +193,7 @@ val cut_and_apply : constr -> unit Proofview.tactic
val apply_in :
advanced_flag -> evars_flag -> clear_flag -> Id.t ->
(clear_flag * constr with_bindings located) list ->
- intro_pattern_expr located option -> unit Proofview.tactic
+ intro_pattern option -> unit Proofview.tactic
(** {6 Elimination tactics. } *)
@@ -270,7 +270,7 @@ val induction : evars_flag ->
(evar_map * constr with_bindings) induction_arg list ->
constr with_bindings option ->
intro_pattern_naming_expr located option *
- or_and_intro_pattern_expr located option ->
+ constr or_and_intro_pattern_expr located option ->
clause option -> unit Proofview.tactic
(** {6 Case analysis tactics. } *)
@@ -283,7 +283,7 @@ val destruct : evars_flag ->
(evar_map * constr with_bindings) induction_arg list ->
constr with_bindings option ->
intro_pattern_naming_expr located option *
- or_and_intro_pattern_expr located option ->
+ constr or_and_intro_pattern_expr located option ->
clause option -> unit Proofview.tactic
(** {6 Generic case analysis / induction tactics. } *)
@@ -293,7 +293,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 *
- or_and_intro_pattern_expr located option))
+ constr or_and_intro_pattern_expr located option))
list *
constr with_bindings option *
clause option -> unit Proofview.tactic
@@ -349,7 +349,7 @@ val assert_before : Name.t -> types -> unit Proofview.tactic
val assert_after : Name.t -> types -> unit Proofview.tactic
val assert_as : (* true = before *) bool ->
- intro_pattern_expr located option -> constr -> unit Proofview.tactic
+ intro_pattern option -> constr -> unit Proofview.tactic
(** Implements the tactics assert, enough and pose proof; note that "by"
applies on the first goal for both assert and enough *)
@@ -364,7 +364,7 @@ val pose_proof : Name.t -> constr ->
(** Common entry point for user-level "assert", "enough" and "pose proof" *)
val forward : bool -> unit Proofview.tactic option ->
- intro_pattern_expr located option -> constr -> unit Proofview.tactic
+ intro_pattern option -> constr -> unit Proofview.tactic
(** Implements the tactic cut, actually a modus ponens rule *)
diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v
index fe4fd179e..92d60c2d3 100644
--- a/theories/Wellfounded/Lexicographic_Exponentiation.v
+++ b/theories/Wellfounded/Lexicographic_Exponentiation.v
@@ -95,8 +95,7 @@ Section Wf_Lexicographic_Exponentiation.
intros.
- inversion H.
assert ([b; a] = ([] ++ [b]) ++ [a]) by auto with sets.
- destruct (app_inj_tail (l ++ [y]) ([] ++ [b]) _ _ H0) as (H6, <-).
- apply app_inj_tail in H6 as (?, <-).
+ destruct (app_inj_tail (l ++ [y]) ([] ++ [b]) _ _ H0) as ((?, <-)/app_inj_tail, <-).
inversion H1; subst; [ apply rt_step; assumption | apply rt_refl ].
- inversion H0.
+ apply app_cons_not_nil in H3 as ().
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 16:26:50 +0000