aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--parsing/g_tactic.ml432
-rw-r--r--parsing/pptactic.ml8
-rw-r--r--parsing/q_coqast.ml46
-rw-r--r--plugins/interface/depends.ml2
-rw-r--r--plugins/interface/xlate.ml4
-rw-r--r--proofs/tacexpr.ml12
-rw-r--r--tactics/hiddentac.ml12
-rw-r--r--tactics/hiddentac.mli4
-rw-r--r--tactics/tacinterp.ml22
-rw-r--r--tactics/tactics.ml10
-rw-r--r--tactics/tactics.mli8
-rw-r--r--test-suite/success/induct.v8
12 files changed, 72 insertions, 56 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 81374e2f25..68e437cab1 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -148,9 +148,9 @@ 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)
- | [([ElimOnIdent id],None,(None,None),None)] ->
+ | [([ElimOnIdent id],None,(None,None))],None ->
TacCase (with_evar,(CRef (Ident id),NoBindings))
| ic ->
TacInductionDestruct (false,with_evar,ic)
@@ -462,7 +462,13 @@ GEXTEND Gram
;
induction_clause:
[ [ lc = LIST1 induction_arg; ipats = with_induction_names;
- el = OPT eliminator; cl = opt_clause -> (lc,el,ipats,cl) ] ]
+ el = OPT eliminator -> (lc,el,ipats) ] ]
+ ;
+ one_induction_clause:
+ [ [ ic = induction_clause; cl = opt_clause -> ([ic],cl) ] ]
+ ;
+ induction_clause_list:
+ [ [ ic = LIST1 induction_clause SEP ","; cl = opt_clause -> (ic,cl) ] ]
;
move_location:
[ [ IDENT "after"; id = id_or_meta -> MoveAfter id
@@ -500,8 +506,8 @@ GEXTEND Gram
| IDENT "eelim"; cl = constr_with_bindings; el = OPT eliminator ->
TacElim (true,cl,el)
| IDENT "elimtype"; c = constr -> TacElimType c
- | IDENT "case"; ic = LIST1 induction_clause SEP "," -> mkTacCase false ic
- | IDENT "ecase"; ic = LIST1 induction_clause SEP "," -> mkTacCase true ic
+ | IDENT "case"; icl = induction_clause_list -> mkTacCase false icl
+ | IDENT "ecase"; icl = induction_clause_list -> mkTacCase true icl
| IDENT "casetype"; c = constr -> TacCaseType c
| "fix"; n = natural -> TacFix (None,n)
| "fix"; id = ident; n = natural -> TacFix (Some id,n)
@@ -556,18 +562,18 @@ GEXTEND Gram
(* Derived basic tactics *)
| IDENT "simple"; IDENT"induction"; h = quantified_hypothesis ->
TacSimpleInductionDestruct (true,h)
- | IDENT "induction"; ic = induction_clause ->
- TacInductionDestruct (true,false,[ic])
- | IDENT "einduction"; ic = induction_clause ->
- TacInductionDestruct(true,true,[ic])
+ | IDENT "induction"; ic = one_induction_clause ->
+ TacInductionDestruct (true,false,ic)
+ | IDENT "einduction"; ic = one_induction_clause ->
+ TacInductionDestruct(true,true,ic)
| IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis;
h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2)
| IDENT "simple"; IDENT "destruct"; h = quantified_hypothesis ->
TacSimpleInductionDestruct (false,h)
- | IDENT "destruct"; ic = LIST1 induction_clause SEP "," ->
- TacInductionDestruct(false,false,ic)
- | IDENT "edestruct"; ic = LIST1 induction_clause SEP "," ->
- TacInductionDestruct(false,true,ic)
+ | IDENT "destruct"; icl = induction_clause_list ->
+ TacInductionDestruct(false,false,icl)
+ | IDENT "edestruct"; icl = induction_clause_list ->
+ TacInductionDestruct(false,true,icl)
| IDENT "decompose"; IDENT "record" ; c = constr -> TacDecomposeAnd c
| IDENT "decompose"; IDENT "sum"; c = constr -> TacDecomposeOr c
| IDENT "decompose"; "["; l = LIST1 smart_global; "]"; c = constr
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index f113908f89..d316a8b05f 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -752,14 +752,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) ->
+ | TacInductionDestruct (isrec,ev,(l,cl)) ->
hov 1 (str (with_evars ev (if isrec then "induction" else "destruct")) ++
spc () ++
- prlist_with_sep pr_coma (fun (h,e,ids,cl) ->
+ prlist_with_sep pr_coma (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 ++
- pr_opt_no_spc (pr_clauses pr_ident) cl) l)
+ pr_opt pr_eliminator e) l ++
+ pr_opt_no_spc (pr_clauses pr_ident) cl)
| TacDoubleInduction (h1,h2) ->
hov 1
(str "double induction" ++
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index cd3e7d2a83..83c4a2fdc6 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -367,13 +367,13 @@ 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_list (mlexpr_of_quadruple
+ $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_option (mlexpr_of_located mlexpr_of_intro_pattern)))))
+ (mlexpr_of_option mlexpr_of_clause) l$ >>
(* Context management *)
| Tacexpr.TacClear (b,l) ->
diff --git a/plugins/interface/depends.ml b/plugins/interface/depends.ml
index 1a5bfaf33d..a8bad4c66b 100644
--- a/plugins/interface/depends.ml
+++ b/plugins/interface/depends.ml
@@ -305,7 +305,7 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
(* Derived basic tactics *)
| TacSimpleInductionDestruct _
| TacDoubleInduction _ -> acc
- | TacInductionDestruct (_, _, [cwbial, cwbo, _, _]) ->
+ | TacInductionDestruct (_, _, ([cwbial, cwbo, _], _)) ->
list_union_map (depends_of_'a_induction_arg depends_of_'constr_with_bindings)
cwbial
(Option.fold_right depends_of_'constr_with_bindings cwbo acc)
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml
index a322c7a72b..613c31db71 100644
--- a/plugins/interface/xlate.ml
+++ b/plugins/interface/xlate.ml
@@ -1229,11 +1229,11 @@ and xlate_tac =
CT_dauto(xlate_int_or_var_opt_to_int_opt a, xlate_int_opt b)
| TacDAuto (a, b, _) ->
xlate_error "TODO: dauto using"
- | TacInductionDestruct(true,false,[a,b,(None,c),None]) ->
+ | TacInductionDestruct(true,false,([a,b,(None,c)],None)) ->
CT_new_destruct
(List.map xlate_int_or_constr a, xlate_using b,
xlate_with_names c)
- | TacInductionDestruct(false,false,[a,b,(None,c),None]) ->
+ | TacInductionDestruct(false,false,([a,b,(None,c)],None)) ->
CT_new_induction
(List.map xlate_int_or_constr a, xlate_using b,
xlate_with_names c)
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index ba3c27e635..c3e12c0dea 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -115,10 +115,12 @@ let goal_location_of = function
| _ ->
error "Not a simple \"in\" clause (one hypothesis or the conclusion)"
-type ('constr,'id) induction_clause =
- ('constr with_bindings induction_arg list * 'constr with_bindings option *
- (intro_pattern_expr located option * intro_pattern_expr located option) *
- 'id gclause option)
+type 'constr induction_clause =
+ ('constr with_bindings induction_arg list * 'constr with_bindings option *
+ (intro_pattern_expr located option * intro_pattern_expr located option))
+
+type ('constr,'id) induction_clause_list =
+ 'constr induction_clause list * 'id gclause option
type multi =
| Precisely of int
@@ -170,7 +172,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
(* Derived basic tactics *)
| TacSimpleInductionDestruct of rec_flag * quantified_hypothesis
- | TacInductionDestruct of rec_flag * evars_flag * ('constr,'id) induction_clause list
+ | TacInductionDestruct of rec_flag * evars_flag * ('constr,'id) induction_clause_list
| TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
| TacDecomposeAnd of 'constr
| TacDecomposeOr of 'constr
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 73aeec501d..d642a38dbc 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -83,12 +83,12 @@ let h_simple_induction_destruct isrec h =
let h_simple_induction = h_simple_induction_destruct true
let h_simple_destruct = h_simple_induction_destruct false
-let h_induction_destruct isrec ev l =
- abstract_tactic (TacInductionDestruct (isrec,ev,List.map (fun (c,e,idl,cl) ->
- List.map inj_ia c,Option.map inj_open_wb e,idl,cl) l))
- (induction_destruct ev isrec l)
-let h_new_induction ev c e idl cl = h_induction_destruct ev true [c,e,idl,cl]
-let h_new_destruct ev c e idl cl = h_induction_destruct ev false [c,e,idl,cl]
+let h_induction_destruct isrec ev (l,cl) =
+ abstract_tactic (TacInductionDestruct (isrec,ev,(List.map (fun (c,e,idl) ->
+ List.map inj_ia c,Option.map inj_open_wb e,idl) l,cl)))
+ (induction_destruct ev isrec (l,cl))
+let h_new_induction ev c e idl cl = h_induction_destruct ev true ([c,e,idl],cl)
+let h_new_destruct ev c e idl cl = h_induction_destruct ev false ([c,e,idl],cl)
let h_specialize n d = abstract_tactic (TacSpecialize (n,inj_open_wb d)) (specialize n d)
let h_lapply c = abstract_tactic (TacLApply (inj_open c)) (cut_and_apply c)
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index f4da57144b..86a3376785 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -78,8 +78,8 @@ val h_new_destruct : evars_flag ->
Tacticals.clause option -> tactic
val h_induction_destruct : rec_flag -> evars_flag ->
(constr with_ebindings induction_arg list * constr with_ebindings option *
- (intro_pattern_expr located option * intro_pattern_expr located option) *
- Tacticals.clause option) list -> tactic
+ (intro_pattern_expr located option * intro_pattern_expr located option)) list
+ * Tacticals.clause option -> tactic
val h_specialize : int option -> constr with_ebindings -> tactic
val h_lapply : constr -> tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 8d8b94c6cb..427a6eaa67 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -736,13 +736,13 @@ let rec intern_atomic lf ist x =
(* Derived basic tactics *)
| TacSimpleInductionDestruct (isrec,h) ->
TacSimpleInductionDestruct (isrec,intern_quantified_hypothesis ist h)
- | TacInductionDestruct (ev,isrec,l) ->
- TacInductionDestruct (ev,isrec,List.map (fun (lc,cbo,(ipato,ipats),cls) ->
+ | 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,
(Option.map (intern_intro_pattern lf ist) ipato,
- Option.map (intern_intro_pattern lf ist) ipats),
- Option.map (clause_app (intern_hyp_location ist)) cls)) l)
+ Option.map (intern_intro_pattern lf ist) ipats))) l,
+ Option.map (clause_app (intern_hyp_location ist)) cls))
| TacDoubleInduction (h1,h2) ->
let h1 = intern_quantified_hypothesis ist h1 in
let h2 = intern_quantified_hypothesis ist h2 in
@@ -2281,14 +2281,14 @@ and interp_atomic ist gl = function
(* Derived basic tactics *)
| TacSimpleInductionDestruct (isrec,h) ->
h_simple_induction_destruct isrec (interp_quantified_hypothesis ist h)
- | TacInductionDestruct (isrec,ev,l) ->
+ | TacInductionDestruct (isrec,ev,(l,cls)) ->
h_induction_destruct ev isrec
- (List.map (fun (lc,cbo,(ipato,ipats),cls) ->
+ (List.map (fun (lc,cbo,(ipato,ipats)) ->
(List.map (interp_induction_arg ist gl) lc,
Option.map (interp_constr_with_bindings ist gl) cbo,
(Option.map (interp_intro_pattern ist gl) ipato,
- Option.map (interp_intro_pattern ist gl) ipats),
- Option.map (interp_clause ist gl) cls)) l)
+ Option.map (interp_intro_pattern ist gl) ipats))) l,
+ Option.map (interp_clause ist gl) cls)
| TacDoubleInduction (h1,h2) ->
let h1 = interp_quantified_hypothesis ist h1 in
let h2 = interp_quantified_hypothesis ist h2 in
@@ -2617,10 +2617,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) ->
- TacInductionDestruct (isrec,ev,List.map (fun (lc,cbo,ids,cls) ->
+ | TacInductionDestruct (isrec,ev,(l,cls)) ->
+ TacInductionDestruct (isrec,ev,(List.map (fun (lc,cbo,ids) ->
List.map (subst_induction_arg subst) lc,
- Option.map (subst_raw_with_bindings subst) cbo, ids, cls) l)
+ Option.map (subst_raw_with_bindings subst) cbo, ids) l, cls))
| TacDoubleInduction (h1,h2) as x -> x
| TacDecomposeAnd c -> TacDecomposeAnd (subst_rawconstr subst c)
| TacDecomposeOr c -> TacDecomposeOr (subst_rawconstr subst c)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8e920ef64a..35f3b40d49 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2919,12 +2919,12 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) =
else induct_destruct_l isrec with_evars lc elim names cls
let induction_destruct isrec with_evars = function
- | [] -> tclIDTAC
- | [a] -> induct_destruct isrec with_evars a
- | a::l ->
+ | [],_ -> tclIDTAC
+ | [a,b,c],cl -> induct_destruct isrec with_evars (a,b,c,cl)
+ | (a,b,c)::l,cl ->
tclTHEN
- (induct_destruct isrec with_evars a)
- (tclMAP (induct_destruct false with_evars) l)
+ (induct_destruct isrec with_evars (a,b,c,cl))
+ (tclMAP (fun (a,b,c) -> induct_destruct false with_evars (a,b,c,cl)) l)
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 40ff0b688e..cedcbf7caa 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -289,12 +289,12 @@ val new_destruct : evars_flag -> constr with_ebindings induction_arg list ->
(*s Generic case analysis / induction tactics. *)
-val induction_destruct : evars_flag -> rec_flag ->
+val induction_destruct : rec_flag -> evars_flag ->
(constr with_ebindings induction_arg list *
constr with_ebindings option *
- (intro_pattern_expr located option * intro_pattern_expr located option) *
- clause option) list ->
- tactic
+ (intro_pattern_expr located option * intro_pattern_expr located option))
+ list *
+ clause option -> tactic
(*s Eliminations giving the type instead of the proof. *)
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index b78651c916..aae55ec7a3 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -32,3 +32,11 @@ Check
Inductive eq2 (A:Type) (a:A)
: forall B C:Type, let D:=(A*B*C)%type in D -> Prop :=
refl2 : eq2 A a unit bool (a,tt,true).
+
+(* Check that induction variables are cleared even with in clause *)
+
+Lemma foo : forall n m : nat, n + m = n + m.
+Proof.
+ intros; induction m as [|m] in n |- *.
+ auto.
+Qed.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 01:18:27 +0000