aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES3
-rw-r--r--doc/refman/RefMan-tac.tex39
-rw-r--r--grammar/q_coqast.ml416
-rw-r--r--intf/tacexpr.mli9
-rw-r--r--parsing/g_tactic.ml438
-rw-r--r--printing/pptactic.ml22
-rw-r--r--tactics/hiddentac.ml8
-rw-r--r--tactics/hiddentac.mli12
-rw-r--r--tactics/tacinterp.ml30
-rw-r--r--tactics/tactics.ml17
-rw-r--r--tactics/tactics.mli4
-rw-r--r--theories/Arith/Compare_dec.v2
-rw-r--r--theories/Arith/Mult.v2
-rw-r--r--theories/Init/Tactics.v8
-rw-r--r--theories/MSets/MSetInterface.v2
-rw-r--r--theories/MSets/MSetList.v6
-rw-r--r--theories/MSets/MSetWeakList.v6
-rw-r--r--theories/Numbers/Integer/BigZ/ZMake.v2
-rw-r--r--theories/Numbers/Natural/Abstract/NDefOps.v2
-rw-r--r--theories/Sorting/Mergesort.v2
-rw-r--r--theories/Structures/OrdersAlt.v6
21 files changed, 122 insertions, 114 deletions
diff --git a/CHANGES b/CHANGES
index 0819cdeed..91e5a33b0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -25,6 +25,9 @@ Tactics
version of "tauto".
- Similarly, "intuition" has been made more uniform and, where it now
fails, "dintuition" can be used.
+- An annotation "eqn:H" or "eqn:?" can be added to a "destruct"
+ or "induction" to make it generate equations in the spirit of "case_eq".
+ The former syntax "_eqn" is discontinued.
Program
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 465ee925e..505db64d0 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1765,7 +1765,7 @@ induction n.
{\tt ($p_{1}$,\ldots,$p_{n}$)} can be used instead of
{\tt [} $p_{1}$ \ldots $p_{n}$ {\tt ]}.
-\item{\tt induction {\term} as {\namingintropattern}}
+\item{\tt induction {\term} eqn:{\namingintropattern}}
This behaves as {\tt induction {\term}} but adds an equation between
{\term} and the value that {\term} takes in each of the induction
@@ -1773,7 +1773,7 @@ induction n.
{\namingintropattern} which can be an identifier, a ``?'', etc, as
indicated in Section~\ref{intros-pattern}.
-\item{\tt induction {\term} as {\namingintropattern} {\disjconjintropattern}}
+\item{\tt induction {\term} as {\disjconjintropattern} eqn:{\namingintropattern}}
This combines the two previous forms.
@@ -1802,7 +1802,7 @@ induction n.
This behaves as {\tt induction {\term$_1$} using {\term$_2$}} but
also providing instances for the premises of the type of {\term$_2$}.
-\item \texttt{induction {\term}$_1$ $\ldots$ {\term}$_n$ using {\qualid}}
+\item \texttt{induction {\term}$_1$, $\ldots$, {\term}$_n$ using {\qualid}}
This syntax is used for the case {\qualid} denotes an induction principle
with complex predicates as the induction principles generated by
@@ -1818,14 +1818,14 @@ induction n.
When an occurrence clause is given, an equation between {\term} and
the value it gets in each case of the induction is added to the
context of the subgoals corresponding to the induction cases (even
- if no clause {\tt as {\namingintropattern}} is given).
+ if no clause {\tt eqn:{\namingintropattern}} is given).
-\item {\tt induction {\term$_1$} with {\bindinglist$_1$} as {\namingintropattern} {\disjconjintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}\\
- {\tt einduction {\term$_1$} with {\bindinglist$_1$} as {\namingintropattern} {\disjconjintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}
+\item {\tt induction {\term$_1$} with {\bindinglist$_1$} as {\disjconjintropattern} eqn:{\namingintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}\\
+ {\tt einduction {\term$_1$} with {\bindinglist$_1$} as {\disjconjintropattern} eqn:{\namingintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}
These are the most general forms of {\tt induction} and {\tt
einduction}. It combines the effects of the {\tt with}, {\tt as},
- {\tt using}, and {\tt in} clauses.
+ {\tt eqn:}, {\tt using}, and {\tt in} clauses.
\item {\tt elim \term}\label{elim}
@@ -1946,6 +1946,10 @@ syntax {\tt destruct ({\num})} (not very interesting anyway).
\end{itemize}
\begin{Variants}
+\item{\tt destruct \term$_1$, \ldots, \term$_n$}
+
+ This is a shortcut for {\tt destruct \term$_1$; \ldots; destruct \term$_n$}.
+
\item{\tt destruct {\term} as {\disjconjintropattern}}
This behaves as {\tt destruct {\term}} but uses the names in
@@ -1964,20 +1968,13 @@ syntax {\tt destruct ({\num})} (not very interesting anyway).
% It is recommended to use this variant of {\tt destruct} for
% robust proof scripts.
-\item{\tt destruct {\term} as {\disjconjintropattern} \_eqn}
+\item{\tt destruct {\term} eqn:{\namingintropattern}}
This behaves as {\tt destruct {\term}} but adds an equation between
{\term} and the value that {\term} takes in each of the possible
- cases. The name of the equation is chosen by Coq. If
- {\disjconjintropattern} is simply {\tt []}, it is automatically considered
- as a disjunctive pattern of the appropriate size.
-
-\item{\tt destruct {\term} as {\disjconjintropattern} \_eqn: {\namingintropattern}}
-
- This behaves as {\tt destruct {\term} as
- {\disjconjintropattern} \_eqn} but use {\namingintropattern} to
- name the equation (see Section~\ref{intros-pattern}). Note that spaces
- can generally be removed around {\tt \_eqn}.
+ cases. The name of the equation is specified by {\namingintropattern}
+ (see Section~\ref{intros-pattern}), in particular {\tt ?} can be
+ used to let Coq generate a fresh name.
\item{\tt destruct {\term} with \bindinglist}
@@ -2011,11 +2008,11 @@ syntax {\tt destruct ({\num})} (not very interesting anyway).
context of the subgoals corresponding to the cases (even
if no clause {\tt as {\namingintropattern}} is given).
-\item{\tt destruct {\term$_1$} with {\bindinglist$_1$} as {\disjconjintropattern} \_eqn: {\namingintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}\\
- {\tt edestruct {\term$_1$} with {\bindinglist$_1$} as {\disjconjintropattern} \_eqn: {\namingintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}
+\item{\tt destruct {\term$_1$} with {\bindinglist$_1$} as {\disjconjintropattern} eqn:{\namingintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}\\
+ {\tt edestruct {\term$_1$} with {\bindinglist$_1$} as {\disjconjintropattern} eqn:{\namingintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}
These are the general forms of {\tt destruct} and {\tt edestruct}.
- They combine the effects of the {\tt with}, {\tt as}, {\tt using},
+ They combine the effects of the {\tt with}, {\tt as}, {\tt eqn:}, {\tt using},
and {\tt in} clauses.
\item{\tt case \term}\label{case}\tacindex{case}
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index c202664e2..3c646c03a 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -359,13 +359,15 @@ let rec mlexpr_of_atomic_tactic = function
$mlexpr_of_quantified_hypothesis h$ >>
| Tacexpr.TacInductionDestruct (isrec,ev,l) ->
<:expr< Tacexpr.TacInductionDestruct $mlexpr_of_bool isrec$ $mlexpr_of_bool ev$
- $mlexpr_of_pair (mlexpr_of_list (mlexpr_of_triple
- (mlexpr_of_list mlexpr_of_induction_arg)
- (mlexpr_of_option mlexpr_of_constr_with_binding)
- (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_clause) l$ >>
+ $mlexpr_of_triple
+ (mlexpr_of_list
+ (mlexpr_of_pair
+ 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_constr_with_binding)
+ (mlexpr_of_option mlexpr_of_clause) l$ >>
(* Context management *)
| Tacexpr.TacClear (b,l) ->
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index ccf682a48..a70ed47d4 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -58,11 +58,14 @@ type 'id message_token =
| MsgIdent of 'id
type 'constr induction_clause =
- ('constr with_bindings induction_arg list * 'constr with_bindings option *
- (intro_pattern_expr located option * intro_pattern_expr located option))
+ 'constr with_bindings induction_arg *
+ (intro_pattern_expr located option (* eqn:... *)
+ * intro_pattern_expr located option) (* as ... *)
type ('constr,'id) induction_clause_list =
- 'constr induction_clause list * 'id clause_expr option
+ 'constr induction_clause list
+ * 'constr with_bindings option (* using ... *)
+ * 'id clause_expr option (* in ... *)
type multi =
| Precisely of int
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 462aa2b46..202512a41 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -134,21 +134,19 @@ let induction_arg_of_constr (c,lbind as clbind) =
else ElimOnConstr clbind
let mkTacCase with_evar = function
- | [([ElimOnConstr cl],None,(None,None))],None ->
+ | [ElimOnConstr cl,(None,None)],None,None ->
TacCase (with_evar,cl)
(* Reinterpret numbers as a notation for terms *)
- | [([(ElimOnAnonHyp n)],None,(None,None))],None ->
+ | [ElimOnAnonHyp n,(None,None)],None,None ->
TacCase (with_evar,
(CPrim (Loc.ghost, Numeral (Bigint.of_string (string_of_int n))),
NoBindings))
(* Reinterpret ident as notations for variables in the context *)
(* because we don't know if they are quantified or not *)
- | [([ElimOnIdent id],None,(None,None))],None ->
+ | [ElimOnIdent id,(None,None)],None,None ->
TacCase (with_evar,(CRef (Ident id),NoBindings))
| ic ->
- if List.exists (fun (cl,a,b) ->
- List.exists (function ElimOnAnonHyp _ -> true | _ -> false) cl)
- (fst ic)
+ if List.exists (function (ElimOnAnonHyp _,_) -> true | _ -> false) (pi1 ic)
then
error "Use of numbers as direct arguments of 'case' is not supported.";
TacInductionDestruct (false,with_evar,ic)
@@ -283,11 +281,6 @@ GEXTEND Gram
| "*" -> loc, IntroForthcoming true
| "**" -> loc, IntroForthcoming false ] ]
;
- intropattern_modifier:
- [ [ IDENT "_eqn";
- id = [ ":"; id = naming_intropattern -> id | -> loc, IntroAnonymous ]
- -> id ] ]
- ;
simple_intropattern:
[ [ pat = disjunctive_intropattern -> pat
| pat = naming_intropattern -> pat
@@ -459,10 +452,12 @@ GEXTEND Gram
[ [ "as"; ipat = simple_intropattern -> Some ipat
| -> None ] ]
;
- with_induction_names:
- [ [ "as"; ipat = simple_intropattern; eq = OPT intropattern_modifier
- -> (eq,Some ipat)
- | -> (None,None) ] ]
+ eqn_ipat:
+ [ [ IDENT "eqn"; ":"; id = naming_intropattern -> Some id
+ | IDENT "_eqn"; ":"; id = naming_intropattern ->
+ let msg = "Obsolete syntax \"_eqn\" could be replaced by \"eqn\"" in
+ msg_warning (strbrk msg); Some id
+ | -> None ] ]
;
as_name:
[ [ "as"; id = ident -> Names.Name id | -> Names.Anonymous ] ]
@@ -491,14 +486,11 @@ GEXTEND Gram
[ [ b = orient; p = rewriter -> let (m,c) = p in (b,m,c) ] ]
;
induction_clause:
- [ [ lc = LIST1 induction_arg; ipats = with_induction_names;
- el = OPT eliminator -> (lc,el,ipats) ] ]
- ;
- one_induction_clause:
- [ [ ic = induction_clause; cl = opt_clause -> ([ic],cl) ] ]
+ [ [ c = induction_arg; pat = as_ipat; eq = eqn_ipat -> (c,(eq,pat)) ] ]
;
induction_clause_list:
- [ [ ic = LIST1 induction_clause SEP ","; cl = opt_clause -> (ic,cl) ] ]
+ [ [ ic = LIST1 induction_clause SEP ",";
+ el = OPT eliminator; cl = opt_clause -> (ic,el,cl) ] ]
;
move_location:
[ [ IDENT "after"; id = id_or_meta -> MoveAfter id
@@ -592,9 +584,9 @@ GEXTEND Gram
(* Derived basic tactics *)
| IDENT "simple"; IDENT"induction"; h = quantified_hypothesis ->
TacSimpleInductionDestruct (true,h)
- | IDENT "induction"; ic = one_induction_clause ->
+ | IDENT "induction"; ic = induction_clause_list ->
TacInductionDestruct (true,false,ic)
- | IDENT "einduction"; ic = one_induction_clause ->
+ | IDENT "einduction"; ic = induction_clause_list ->
TacInductionDestruct(true,true,ic)
| IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis;
h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 815ee6e5c..e1575eab7 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -338,11 +338,15 @@ let pr_bindings prlc prc = pr_bindings_gen false prlc prc
let pr_with_bindings prlc prc (c,bl) =
hov 1 (prc c ++ pr_bindings prlc prc bl)
+let pr_as_ipat pat = str "as " ++ pr_intro_pattern pat
+let pr_eqn_ipat pat = str "eqn:" ++ pr_intro_pattern pat
+
let pr_with_induction_names = function
| None, None -> mt ()
- | eqpat, ipat ->
- spc () ++ hov 1 (str "as" ++ pr_opt pr_intro_pattern eqpat ++
- pr_opt pr_intro_pattern ipat)
+ | Some eqpat, None -> spc () ++ hov 1 (pr_eqn_ipat eqpat)
+ | None, Some ipat -> spc () ++ hov 1 (pr_as_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 () ++ pr_intro_pattern ipat)
@@ -714,14 +718,14 @@ and pr_atom1 = function
| TacSimpleInductionDestruct (isrec,h) ->
hov 1 (str "simple " ++ str (if isrec then "induction" else "destruct")
++ pr_arg pr_quantified_hypothesis h)
- | TacInductionDestruct (isrec,ev,(l,cl)) ->
+ | TacInductionDestruct (isrec,ev,(l,el,cl)) ->
hov 1 (str (with_evars ev (if isrec then "induction" else "destruct")) ++
spc () ++
- prlist_with_sep pr_comma (fun (h,e,ids) ->
- prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++
- pr_with_induction_names ids ++
- pr_opt pr_eliminator e) l ++
- pr_opt_no_spc (pr_clauses None pr_ident) cl)
+ prlist_with_sep pr_comma (fun (h,ids) ->
+ pr_induction_arg pr_lconstr pr_constr h ++
+ pr_with_induction_names ids) l ++
+ pr_opt pr_eliminator el ++
+ pr_opt_no_spc (pr_clauses None pr_ident) cl)
| TacDoubleInduction (h1,h2) ->
hov 1
(str "double induction" ++
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index d5ee78fea..20b70cef4 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -84,12 +84,12 @@ let out_indarg = function
| ElimOnAnonHyp n -> ElimOnAnonHyp n
let h_induction_destruct isrec ev lcl =
- let lcl' = on_fst (List.map (fun (a,b,c) ->(List.map out_indarg a,b,c))) lcl in
+ let lcl' = on_pi1 (List.map (fun (a,b) ->(out_indarg a,b))) lcl in
abstract_tactic (TacInductionDestruct (isrec,ev,lcl'))
(induction_destruct isrec ev lcl)
-let h_new_induction ev c e idl cl =
- h_induction_destruct true ev ([c,e,idl],cl)
-let h_new_destruct ev c e idl cl = h_induction_destruct false ev ([c,e,idl],cl)
+let h_new_induction ev c idl e cl =
+ h_induction_destruct true ev ([c,idl],e,cl)
+let h_new_destruct ev c idl e cl = h_induction_destruct false ev ([c,idl],e,cl)
let h_specialize n d = abstract_tactic (TacSpecialize (n,d)) (specialize n d)
let h_lapply c = abstract_tactic (TacLApply c) (cut_and_apply c)
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index cffe84252..3028d3a1e 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -68,19 +68,19 @@ val h_simple_induction : quantified_hypothesis -> tactic
val h_simple_destruct : quantified_hypothesis -> tactic
val h_simple_induction_destruct : rec_flag -> quantified_hypothesis -> tactic
val h_new_induction : evars_flag ->
- (evar_map * constr with_bindings) induction_arg list ->
- constr with_bindings option ->
+ (evar_map * constr with_bindings) induction_arg ->
intro_pattern_expr located option * intro_pattern_expr located option ->
+ constr with_bindings option ->
Locus.clause option -> tactic
val h_new_destruct : evars_flag ->
- (evar_map * constr with_bindings) induction_arg list ->
- constr with_bindings option ->
+ (evar_map * constr with_bindings) induction_arg ->
intro_pattern_expr located option * intro_pattern_expr located option ->
+ constr with_bindings option ->
Locus.clause option -> tactic
val h_induction_destruct : rec_flag -> evars_flag ->
- ((evar_map * constr with_bindings) induction_arg list *
- constr with_bindings option *
+ ((evar_map * constr with_bindings) induction_arg *
(intro_pattern_expr located option * intro_pattern_expr located option)) list
+ * constr with_bindings option
* Locus.clause option -> tactic
val h_specialize : int option -> constr with_bindings -> tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 2beba9888..3eddb1aae 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -732,12 +732,12 @@ let rec intern_atomic lf ist x =
(* Derived basic tactics *)
| TacSimpleInductionDestruct (isrec,h) ->
TacSimpleInductionDestruct (isrec,intern_quantified_hypothesis ist h)
- | TacInductionDestruct (ev,isrec,(l,cls)) ->
- TacInductionDestruct (ev,isrec,(List.map (fun (lc,cbo,(ipato,ipats)) ->
- (List.map (intern_induction_arg ist) lc,
- Option.map (intern_constr_with_bindings ist) cbo,
+ | 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_constr_with_bindings ist) el,
Option.map (clause_app (intern_hyp_location ist)) cls))
| TacDoubleInduction (h1,h2) ->
let h1 = intern_quantified_hypothesis ist h1 in
@@ -2424,17 +2424,17 @@ and interp_atomic ist gl tac =
(* Derived basic tactics *)
| TacSimpleInductionDestruct (isrec,h) ->
h_simple_induction_destruct isrec (interp_quantified_hypothesis ist h)
- | TacInductionDestruct (isrec,ev,(l,cls)) ->
+ | TacInductionDestruct (isrec,ev,(l,el,cls)) ->
let sigma, l =
- list_fold_map (fun sigma (lc,cbo,(ipato,ipats)) ->
- let lc = List.map (interp_induction_arg ist gl) lc in
- let sigma,cbo =
- Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in
- (sigma,(lc,cbo,
+ list_fold_map (fun sigma (c,(ipato,ipats)) ->
+ let c = interp_induction_arg ist gl c in
+ (sigma,(c,
(Option.map (interp_intro_pattern ist gl) ipato,
Option.map (interp_intro_pattern ist gl) ipats)))) sigma l in
+ let sigma,el =
+ Option.fold_map (interp_constr_with_bindings ist env) sigma el in
let cls = Option.map (interp_clause ist gl) cls in
- tclWITHHOLES ev (h_induction_destruct isrec ev) sigma (l,cls)
+ tclWITHHOLES ev (h_induction_destruct isrec ev) sigma (l,el,cls)
| TacDoubleInduction (h1,h2) ->
let h1 = interp_quantified_hypothesis ist h1 in
let h2 = interp_quantified_hypothesis ist h2 in
@@ -2862,10 +2862,10 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
(* Derived basic tactics *)
| TacSimpleInductionDestruct (isrec,h) as x -> x
- | TacInductionDestruct (isrec,ev,(l,cls)) ->
- TacInductionDestruct (isrec,ev,(List.map (fun (lc,cbo,ids) ->
- List.map (subst_induction_arg subst) lc,
- Option.map (subst_glob_with_bindings subst) cbo, ids) l, cls))
+ | TacInductionDestruct (isrec,ev,(l,el,cls)) ->
+ let l' = List.map (fun (c,ids) -> subst_induction_arg subst c, ids) l in
+ let el' = Option.map (subst_glob_with_bindings subst) el in
+ TacInductionDestruct (isrec,ev,(l',el',cls))
| TacDoubleInduction (h1,h2) as x -> x
| TacDecomposeAnd c -> TacDecomposeAnd (subst_glob_constr subst c)
| TacDecomposeOr c -> TacDecomposeOr (subst_glob_constr subst c)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ad44171da..44bda9aac 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3207,12 +3207,19 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) gl =
end
let induction_destruct isrec with_evars = function
- | [],_ -> tclIDTAC
- | [a,b,c],cl -> induct_destruct isrec with_evars (a,b,c,cl)
- | (a,b,c)::l,cl ->
+ | [],_,_ -> tclIDTAC
+ | [a,b],el,cl -> induct_destruct isrec with_evars ([a],el,b,cl)
+ | (a,b)::l,None,cl ->
tclTHEN
- (induct_destruct isrec with_evars (a,b,c,cl))
- (tclMAP (fun (a,b,c) -> induct_destruct false with_evars (a,b,c,cl)) l)
+ (induct_destruct isrec with_evars ([a],None,b,cl))
+ (tclMAP (fun (a,b) -> induct_destruct false with_evars ([a],None,b,cl)) l)
+ | l,Some el,cl ->
+ let check_basic_using = function
+ | a,(None,None) -> a
+ | _ -> error "Unsupported syntax for \"using\"."
+ in
+ let l' = List.map check_basic_using l in
+ induct_destruct isrec with_evars (l', Some el, (None,None), cl)
let new_induct ev lc e idl cls = induct_destruct true ev (lc,e,idl,cls)
let new_destruct ev lc e idl cls = induct_destruct false ev (lc,e,idl,cls)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 6cdac9d55..b1abb67a9 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -295,10 +295,10 @@ val new_destruct : evars_flag ->
(** {6 Generic case analysis / induction tactics. } *)
val induction_destruct : rec_flag -> evars_flag ->
- ((evar_map * constr with_bindings) induction_arg list *
- constr with_bindings option *
+ ((evar_map * constr with_bindings) induction_arg *
(intro_pattern_expr located option * intro_pattern_expr located option))
list *
+ constr with_bindings option *
clause option -> tactic
(** {6 Eliminations giving the type instead of the proof. } *)
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index f6801da20..d7dd987fb 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -202,7 +202,7 @@ Lemma nat_compare_spec :
forall x y, CompareSpec (x=y) (x<y) (y<x) (nat_compare x y).
Proof.
intros.
- destruct (nat_compare x y) as [ ]_eqn; constructor.
+ destruct (nat_compare x y) eqn:?; constructor.
apply nat_compare_eq; auto.
apply <- nat_compare_lt; auto.
apply <- nat_compare_gt; auto.
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index 0c44cfaf1..f779e0772 100644
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -73,7 +73,7 @@ Qed.
Lemma mult_minus_distr_r : forall n m p, (n - m) * p = n * p - m * p.
Proof.
- intros; induction n m using nat_double_ind; simpl; auto with arith.
+ intros; induction n, m using nat_double_ind; simpl; auto with arith.
rewrite <- minus_plus_simpl_l_reverse; auto with arith.
Qed.
Hint Resolve mult_minus_distr_r: arith v62.
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 9b2a026c2..ad332a947 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -84,13 +84,13 @@ Ltac destr_eq H := discriminate H || (try (injection H; clear H; intro H)).
(* Similar variants of destruct *)
Tactic Notation "destruct_with_eqn" constr(x) :=
- destruct x as []_eqn.
+ destruct x eqn:?.
Tactic Notation "destruct_with_eqn" ident(n) :=
- try intros until n; destruct n as []_eqn.
+ try intros until n; destruct n eqn:?.
Tactic Notation "destruct_with_eqn" ":" ident(H) constr(x) :=
- destruct x as []_eqn:H.
+ destruct x eqn:H.
Tactic Notation "destruct_with_eqn" ":" ident(H) ident(n) :=
- try intros until n; destruct n as []_eqn:H.
+ try intros until n; destruct n eqn:H.
(** Break every hypothesis of a certain type *)
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index f2b908af0..6778deffa 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -480,7 +480,7 @@ Module WRaw2SetsOn (E:DecidableType)(M:WRawSets E) <: WSetsOn E.
Proof.
intros (s,Hs) (s',Hs').
change ({M.Equal s s'}+{~M.Equal s s'}).
- destruct (M.equal s s') as [ ]_eqn:H; [left|right];
+ destruct (M.equal s s') eqn:H; [left|right];
rewrite <- M.equal_spec; congruence.
Defined.
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index bcf68f1d4..d9b1fd9bb 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -662,7 +662,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
Proof.
induction s; simpl; intros.
split; intuition; inv.
- destruct (f a) as [ ]_eqn:F; rewrite !InA_cons, ?IHs; intuition.
+ destruct (f a) eqn:F; rewrite !InA_cons, ?IHs; intuition.
setoid_replace x with a; auto.
setoid_replace a with x in F; auto; congruence.
Qed.
@@ -674,7 +674,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
Proof.
unfold For_all; induction s; simpl; intros.
split; intros; auto. inv.
- destruct (f a) as [ ]_eqn:F.
+ destruct (f a) eqn:F.
rewrite IHs; auto. firstorder. inv; auto.
setoid_replace x with a; auto.
split; intros H'. discriminate.
@@ -688,7 +688,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
Proof.
unfold Exists; induction s; simpl; intros.
firstorder. discriminate. inv.
- destruct (f a) as [ ]_eqn:F.
+ destruct (f a) eqn:F.
firstorder.
rewrite IHs; auto.
firstorder.
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v
index 76f09c76e..fd4114cd4 100644
--- a/theories/MSets/MSetWeakList.v
+++ b/theories/MSets/MSetWeakList.v
@@ -396,7 +396,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
induction s; simpl.
intuition; inv.
intros.
- destruct (f a) as [ ]_eqn:E; rewrite ?InA_cons, IHs; intuition.
+ destruct (f a) eqn:E; rewrite ?InA_cons, IHs; intuition.
setoid_replace x with a; auto.
setoid_replace a with x in E; auto. congruence.
Qed.
@@ -420,7 +420,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
unfold For_all; induction s; simpl.
intuition. inv.
intros; inv.
- destruct (f a) as [ ]_eqn:F.
+ destruct (f a) eqn:F.
rewrite IHs; intuition. inv; auto.
setoid_replace x with a; auto.
split; intros H'; try discriminate.
@@ -436,7 +436,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
unfold Exists; induction s; simpl.
split; [discriminate| intros (x & Hx & _); inv].
intros.
- destruct (f a) as [ ]_eqn:F.
+ destruct (f a) eqn:F.
split; auto.
exists a; auto.
rewrite IHs; firstorder.
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index d1c817f54..6b4e154c0 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -416,7 +416,7 @@ Module Make (NN:NType) <: ZType.
Ltac break_nonneg x px EQx :=
let H := fresh "H" in
assert (H:=NN.spec_pos x);
- destruct (NN.to_Z x) as [|px|px]_eqn:EQx;
+ destruct (NN.to_Z x) as [|px|px] eqn:EQx;
[clear H|clear H|elim H; reflexivity].
Theorem spec_div_eucl: forall x y,
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index ad7a9f3ae..cabba1131 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -376,7 +376,7 @@ Lemma log_good_step : forall n h1 h2,
(if n << 2 then 0 else S (h2 (half n))).
Proof.
intros n h1 h2 E.
-destruct (n<<2) as [ ]_eqn:H.
+destruct (n<<2) eqn:H.
auto with *.
f_equiv. apply E, half_decrease.
rewrite two_succ, <- not_true_iff_false, ltb_lt, nlt_ge, le_succ_l in H.
diff --git a/theories/Sorting/Mergesort.v b/theories/Sorting/Mergesort.v
index 7124cd536..695291b8c 100644
--- a/theories/Sorting/Mergesort.v
+++ b/theories/Sorting/Mergesort.v
@@ -131,7 +131,7 @@ Theorem Sorted_merge : forall l1 l2,
Sorted l1 -> Sorted l2 -> Sorted (merge l1 l2).
Proof.
induction l1; induction l2; intros; simpl; auto.
- destruct (a <=? a0) as ()_eqn:Heq1.
+ destruct (a <=? a0) eqn:Heq1.
invert H.
simpl. constructor; trivial; rewrite Heq1; constructor.
assert (Sorted (merge (b::l) (a0::l2))) by (apply IHl1; auto).
diff --git a/theories/Structures/OrdersAlt.v b/theories/Structures/OrdersAlt.v
index 85e7fb176..5dd917a71 100644
--- a/theories/Structures/OrdersAlt.v
+++ b/theories/Structures/OrdersAlt.v
@@ -140,7 +140,7 @@ Module OT_from_Alt (Import O:OrderedTypeAlt) <: OrderedType.
Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z.
Proof.
unfold lt, eq; intros x y z Hxy Hyz.
- destruct (compare x z) as [ ]_eqn:Hxz; auto.
+ destruct (compare x z) eqn:Hxz; auto.
rewrite compare_sym, CompOpp_iff in Hyz. simpl in Hyz.
rewrite (compare_trans Hxz Hyz) in Hxy; discriminate.
rewrite compare_sym, CompOpp_iff in Hxy. simpl in Hxy.
@@ -150,7 +150,7 @@ Module OT_from_Alt (Import O:OrderedTypeAlt) <: OrderedType.
Lemma eq_lt : forall x y z, eq x y -> lt y z -> lt x z.
Proof.
unfold lt, eq; intros x y z Hxy Hyz.
- destruct (compare x z) as [ ]_eqn:Hxz; auto.
+ destruct (compare x z) eqn:Hxz; auto.
rewrite compare_sym, CompOpp_iff in Hxy. simpl in Hxy.
rewrite (compare_trans Hxy Hxz) in Hyz; discriminate.
rewrite compare_sym, CompOpp_iff in Hyz. simpl in Hyz.
@@ -169,7 +169,7 @@ Module OT_from_Alt (Import O:OrderedTypeAlt) <: OrderedType.
Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
Proof.
unfold eq, lt, compare; intros.
- destruct (O.compare x y) as [ ]_eqn:H; auto.
+ destruct (O.compare x y) eqn:H; auto.
apply CompGt.
rewrite compare_sym, H; auto.
Qed.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 01:25:48 +0000