Add "case as/in/using" and temporary "destruct" with n args.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12347 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 18 insertions, 8 deletions

diff --git a/CHANGES b/CHANGES
index 3a471e9478..ecf61370d5 100644
--- a/CHANGES
+++ b/CHANGES
@@ -29,13 +29,15 @@ Tactics
 - New variant "subst'" of "subst" that supports JMeq.
 - New tactic "decide lemma with hyp" for rewriting decidability lemmas
   when one knows which side is true.
-- Tactic "exists" and "eexists" supports iteration using
-  comma-separated arguments.
+- Tactic "exists", "eexists", "destruct" and "edestruct" supports iteration
+  using comma-separated arguments.
 - Tactic "gappa" has been removed from the Dp plugin.
 - Tactic "firstorder" now supports the combination of its "using" and
   "with" options.
 - An inductive type as argument of the "using" option of "auto/eauto/firstorder"
   is interpreted as using the collection of its constructors.
+- Tactic names "case" and "elim" now support clauses "as" and "in" and become
+  then synonymous of "destruct" and "induction" respectively.
 
 Tactic Language
 
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index c61bff02d7..81374e2f25 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -147,6 +147,14 @@ let induction_arg_of_constr (c,lbind as clbind) =
     with _ -> ElimOnConstr clbind
   else ElimOnConstr clbind
 
+let mkTacCase with_evar = function
+  | [([ElimOnConstr cl],None,(None,None),None)] ->
+      TacCase (with_evar,cl)
+  | [([ElimOnIdent id],None,(None,None),None)] ->
+      TacCase (with_evar,(CRef (Ident id),NoBindings))
+  | ic ->
+      TacInductionDestruct (false,with_evar,ic)
+
 let rec mkCLambdaN_simple_loc loc bll c =
   match bll with
   | ((loc1,_)::_ as idl,bk,t) :: bll ->
@@ -492,8 +500,8 @@ GEXTEND Gram
       | IDENT "eelim"; cl = constr_with_bindings; el = OPT eliminator ->
           TacElim (true,cl,el)
       | IDENT "elimtype"; c = constr -> TacElimType c
-      | IDENT "case"; cl = constr_with_bindings -> TacCase (false,cl)
-      | IDENT "ecase"; cl = constr_with_bindings -> TacCase (true,cl)
+      | IDENT "case"; ic = LIST1 induction_clause SEP "," -> mkTacCase false ic
+      | IDENT "ecase"; ic = LIST1 induction_clause SEP "," -> mkTacCase true ic
       | IDENT "casetype"; c = constr -> TacCaseType c
       | "fix"; n = natural -> TacFix (None,n)
       | "fix"; id = ident; n = natural -> TacFix (Some id,n)
@@ -556,10 +564,10 @@ GEXTEND Gram
 	  h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2)
       | IDENT "simple"; IDENT "destruct"; h = quantified_hypothesis ->
           TacSimpleInductionDestruct (false,h)
-      | IDENT "destruct"; ic = induction_clause ->
-	  TacInductionDestruct(false,false,[ic])
-      | IDENT "edestruct";  ic = induction_clause ->
-	  TacInductionDestruct(false,true,[ic])
+      | IDENT "destruct"; ic = LIST1 induction_clause SEP "," ->
+	  TacInductionDestruct(false,false,ic)
+      | IDENT "edestruct";  ic = LIST1 induction_clause SEP "," ->
+	  TacInductionDestruct(false,true,ic)
       | IDENT "decompose"; IDENT "record" ; c = constr -> TacDecomposeAnd c
       | IDENT "decompose"; IDENT "sum"; c = constr -> TacDecomposeOr c
       | IDENT "decompose"; "["; l = LIST1 smart_global; "]"; c = constr