From dfa81d7860309029d100cd5348d2dd6bd8fa33c9 Mon Sep 17 00:00:00 2001 From: jforest Date: Tue, 21 Mar 2006 21:54:43 +0000 Subject: + destruct now works as induction on multiple arguments : destruct x y z using scheme + replace c1 with c2 has now a new optional argument replace c1 with c2 by tac tries to prove c2 = c1 with tac + I've also factorize the code correspoing to replace in extractactics git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8651 85f007b7-540e-0410-9357-904b9bb8a0f7 --- proofs/tacexpr.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs') diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 42a5d5cbe2..ea7c49f2bc 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -141,7 +141,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacNewInduction of 'constr induction_arg list * 'constr with_bindings option * intro_pattern_expr | TacSimpleDestruct of quantified_hypothesis - | TacNewDestruct of 'constr induction_arg * 'constr with_bindings option + | TacNewDestruct of 'constr induction_arg list * 'constr with_bindings option * intro_pattern_expr | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis -- cgit v1.2.3