Ajout de eelim, ecase, edestruct et einduction (expérimental).

Ajout de l'option with à (e)destruct et (e)induction.



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

3 files changed, 44 insertions, 34 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 3f7c8c3e8e..e8d1be4f63 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -111,9 +111,11 @@ let mk_cofix_tac (loc,id,bl,ann,ty) =
   (id,CProdN(loc,bl,ty))
 
 (* Functions overloaded by quotifier *)
-let induction_arg_of_constr c =
-  try ElimOnIdent (constr_loc c,snd(coerce_to_id c))
-  with _ -> ElimOnConstr c
+let induction_arg_of_constr (c,lbind as clbind) =
+  if lbind = NoBindings then
+    try ElimOnIdent (constr_loc c,snd(coerce_to_id c))
+    with _ -> ElimOnConstr clbind
+  else ElimOnConstr clbind
 
 (* Auxiliary grammar rules *)
 
@@ -147,7 +149,7 @@ GEXTEND Gram
   ;
   induction_arg:
     [ [ n = natural -> ElimOnAnonHyp n
-      | c = constr -> induction_arg_of_constr c
+      | c = constr_with_bindings -> induction_arg_of_constr c
     ] ]
   ;
   quantified_hypothesis:
@@ -343,9 +345,12 @@ GEXTEND Gram
       | IDENT "apply"; cl = constr_with_bindings -> TacApply (false,cl)
       | IDENT "eapply"; cl = constr_with_bindings -> TacApply (true,cl)
       | IDENT "elim"; cl = constr_with_bindings; el = OPT eliminator ->
-          TacElim (cl,el)
+          TacElim (false,cl,el)
+      | 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 cl
+      | IDENT "case"; cl = constr_with_bindings -> TacCase (false,cl)
+      | IDENT "ecase"; cl = constr_with_bindings -> TacCase (true,cl)
       | IDENT "casetype"; c = constr -> TacCaseType c
       | "fix"; n = natural -> TacFix (None,n)
       | "fix"; id = ident; n = natural -> TacFix (Some id,n)
@@ -389,13 +394,17 @@ GEXTEND Gram
       | IDENT "simple"; IDENT"induction"; h = quantified_hypothesis ->
           TacSimpleInduction h
       | IDENT "induction"; lc = LIST1 induction_arg; ids = with_names; 
-	  el = OPT eliminator -> TacNewInduction (lc,el,ids)
+	  el = OPT eliminator -> TacNewInduction (false,lc,el,ids)
+      | IDENT "einduction"; lc = LIST1 induction_arg; ids = with_names; 
+	  el = OPT eliminator -> TacNewInduction (true,lc,el,ids)
       | IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis;
 	  h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2)
-      | IDENT "simple"; IDENT"destruct"; h = quantified_hypothesis ->
+      | IDENT "simple"; IDENT "destruct"; h = quantified_hypothesis ->
           TacSimpleDestruct h
       | IDENT "destruct"; lc = LIST1 induction_arg; ids = with_names; 
-	  el = OPT eliminator -> TacNewDestruct (lc,el,ids)
+	  el = OPT eliminator -> TacNewDestruct (false,lc,el,ids)
+      | IDENT "edestruct"; lc = LIST1 induction_arg; ids = with_names; 
+	  el = OPT eliminator -> TacNewDestruct (true,lc,el,ids)
       | 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 c6c168d4ed..0190635273 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -427,8 +427,8 @@ let pr_clause_pattern pr_id = function
 
 let pr_orient b = if b then mt () else str " <-"
 
-let pr_induction_arg prc = function
-  | ElimOnConstr c -> prc c
+let pr_induction_arg prlc prc = function
+  | ElimOnConstr c -> pr_with_bindings prlc prc c
   | ElimOnIdent (loc,id) -> pr_with_comments loc (pr_id id)
   | ElimOnAnonHyp n -> int n
 
@@ -680,11 +680,12 @@ and pr_atom1 = function
   | TacApply (ev,cb) ->
       hov 1 (str (if ev then "eapply" else "apply") ++ spc () ++ 
              pr_with_bindings cb)
-  | TacElim (cb,cbo) ->
-      hov 1 (str "elim" ++ pr_arg pr_with_bindings cb ++ 
+  | TacElim (ev,cb,cbo) ->
+      hov 1 (str (if ev then "eelim" else "elim") ++ pr_arg pr_with_bindings cb ++ 
         pr_opt pr_eliminator cbo)
   | TacElimType c -> hov 1 (str "elimtype" ++ pr_constrarg c)
-  | TacCase cb -> hov 1 (str "case" ++ spc () ++ pr_with_bindings cb)
+  | TacCase (ev,cb) ->
+      hov 1 (str (if ev then "ecase" else "case") ++ spc () ++ pr_with_bindings cb)
   | TacCaseType c -> hov 1 (str "casetype" ++ pr_constrarg c)
   | TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n)
   | TacMutualFix (id,n,l) ->
@@ -726,16 +727,16 @@ and pr_atom1 = function
   (* Derived basic tactics *)
   | TacSimpleInduction h ->
       hov 1 (str "simple induction" ++ pr_arg pr_quantified_hypothesis h)
-  | TacNewInduction (h,e,ids) ->
-      hov 1 (str "induction" ++ spc () ++
-	     prlist_with_sep spc (pr_induction_arg pr_constr) h ++
+  | TacNewInduction (ev,h,e,ids) ->
+      hov 1 (str (if ev then "einduction" else "induction") ++ spc () ++
+	     prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++
 	     pr_with_names ids ++
              pr_opt pr_eliminator e)
   | TacSimpleDestruct h ->
       hov 1 (str "simple destruct" ++ pr_arg pr_quantified_hypothesis h)
-  | TacNewDestruct (h,e,ids) ->
-      hov 1 (str "destruct" ++ spc () ++
-             prlist_with_sep spc (pr_induction_arg pr_constr) h ++ 
+  | TacNewDestruct (ev,h,e,ids) ->
+      hov 1 (str (if ev then "edestruct" else "destruct") ++ spc () ++
+             prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++ 
 	     pr_with_names ids ++
              pr_opt pr_eliminator e)
   | TacDoubleInduction (h1,h2) ->
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 4b1dfd9e36..fbd2e6e077 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -227,19 +227,19 @@ let mlexpr_of_binding_kind = function
   | Rawterm.NoBindings -> 
        <:expr< Rawterm.NoBindings >>
 
+let mlexpr_of_binding = mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_constr
+
+let mlexpr_of_constr_with_binding =
+  mlexpr_of_pair mlexpr_of_constr mlexpr_of_binding_kind
+
 let mlexpr_of_induction_arg = function
   | Tacexpr.ElimOnConstr c ->
-      <:expr< Tacexpr.ElimOnConstr $mlexpr_of_constr c$ >>
+      <:expr< Tacexpr.ElimOnConstr $mlexpr_of_constr_with_binding c$ >>
   | Tacexpr.ElimOnIdent (_,id) -> 
       <:expr< Tacexpr.ElimOnIdent $dloc$ $mlexpr_of_ident id$ >>
   | Tacexpr.ElimOnAnonHyp n ->
       <:expr< Tacexpr.ElimOnAnonHyp $mlexpr_of_int n$ >>
 
-let mlexpr_of_binding = mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_constr
-
-let mlexpr_of_constr_with_binding =
-  mlexpr_of_pair mlexpr_of_constr mlexpr_of_binding_kind
-
 let mlexpr_of_clause_pattern _ = failwith "mlexpr_of_clause_pattern: TODO"
 
 let mlexpr_of_pattern_ast = mlexpr_of_constr
@@ -287,15 +287,15 @@ let rec mlexpr_of_atomic_tactic = function
       <:expr< Tacexpr.TacVmCastNoCheck $mlexpr_of_constr c$ >>
   | Tacexpr.TacApply (false,cb) ->
       <:expr< Tacexpr.TacApply False $mlexpr_of_constr_with_binding cb$ >>
-  | Tacexpr.TacElim (cb,cbo) ->
+  | Tacexpr.TacElim (false,cb,cbo) ->
       let cb = mlexpr_of_constr_with_binding cb in
       let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
-      <:expr< Tacexpr.TacElim $cb$ $cbo$ >>
+      <:expr< Tacexpr.TacElim False $cb$ $cbo$ >>
   | Tacexpr.TacElimType c ->
       <:expr< Tacexpr.TacElimType $mlexpr_of_constr c$ >>
-  | Tacexpr.TacCase cb ->
+  | Tacexpr.TacCase (false,cb) ->
       let cb = mlexpr_of_constr_with_binding cb in
-      <:expr< Tacexpr.TacCase $cb$ >>
+      <:expr< Tacexpr.TacCase False $cb$ >>
   | Tacexpr.TacCaseType c ->
       <:expr< Tacexpr.TacCaseType $mlexpr_of_constr c$ >>
   | Tacexpr.TacFix (ido,n) ->
@@ -335,18 +335,18 @@ let rec mlexpr_of_atomic_tactic = function
   (* Derived basic tactics *)
   | Tacexpr.TacSimpleInduction h ->
       <:expr< Tacexpr.TacSimpleInduction ($mlexpr_of_quantified_hypothesis h$) >>
-  | Tacexpr.TacNewInduction (cl,cbo,ids) ->
+  | Tacexpr.TacNewInduction (false,cl,cbo,ids) ->
       let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
       let ids = mlexpr_of_intro_pattern ids in
 (*       let ids = mlexpr_of_option mlexpr_of_intro_pattern ids in *)
 (*       <:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ $cbo$ $ids$>> *)
-      <:expr< Tacexpr.TacNewInduction $mlexpr_of_list mlexpr_of_induction_arg cl$ $cbo$ $ids$>>
+      <:expr< Tacexpr.TacNewInduction False $mlexpr_of_list mlexpr_of_induction_arg cl$ $cbo$ $ids$>>
   | Tacexpr.TacSimpleDestruct h ->
       <:expr< Tacexpr.TacSimpleDestruct $mlexpr_of_quantified_hypothesis h$ >>
-  | Tacexpr.TacNewDestruct (c,cbo,ids) ->
+  | Tacexpr.TacNewDestruct (false,c,cbo,ids) ->
       let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
       let ids = mlexpr_of_intro_pattern ids in
-      <:expr< Tacexpr.TacNewDestruct $mlexpr_of_list mlexpr_of_induction_arg c$ $cbo$ $ids$ >>
+      <:expr< Tacexpr.TacNewDestruct False $mlexpr_of_list mlexpr_of_induction_arg c$ $cbo$ $ids$ >>
 
   (* Context management *)
   | Tacexpr.TacClear (b,l) ->