Uniformisation des politiques de nommage de NewDestruct sur arguments recursifs et Induction style Hrec; mise en place systeme de traduction automatique; Elim/Case reconnaissent les premisses nommees du but

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

4 files changed, 16 insertions, 16 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 01b59dcf65..2416b14bd5 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -309,14 +309,14 @@ GEXTEND Gram
       | IDENT "LApply"; c = constr -> TacLApply c
 
       (* Derived basic tactics *)
-      | IDENT "Induction"; h = quantified_hypothesis -> TacSimpleInduction h
+      | IDENT "Induction"; h = quantified_hypothesis -> TacSimpleInduction (h,ref [])
       | IDENT "NewInduction"; c = induction_arg; el = OPT eliminator;
-          ids = with_names -> TacNewInduction (c,el,ids)
+          ids = with_names -> TacNewInduction (c,el,(ids,ref []))
       | IDENT "Double"; IDENT "Induction"; h1 = quantified_hypothesis;
 	  h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2)
       | IDENT "Destruct"; h = quantified_hypothesis -> TacSimpleDestruct h
       | IDENT "NewDestruct"; c = induction_arg; el = OPT eliminator; 
-          ids = with_names -> TacNewDestruct (c,el,ids)
+          ids = with_names -> TacNewDestruct (c,el,(ids,ref []))
       | IDENT "Decompose"; IDENT "Record" ; c = constr -> TacDecomposeAnd c
       | IDENT "Decompose"; IDENT "Sum"; c = constr -> TacDecomposeOr c
       | IDENT "Decompose"; "["; l = LIST1 global_or_ltac_ref; "]"; c = constr
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 8151a8c14f..9ee0041804 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -352,15 +352,15 @@ GEXTEND Gram
 
       (* Derived basic tactics *)
       | IDENT "simple"; IDENT"induction"; h = quantified_hypothesis ->
-          TacSimpleInduction h
+          TacSimpleInduction (h,ref [])
       | IDENT "induction"; c = induction_arg; ids = with_names; 
-	  el = OPT eliminator -> TacNewInduction (c,el,ids)
+	  el = OPT eliminator -> TacNewInduction (c,el,(ids,ref []))
       | IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis;
 	  h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2)
       | IDENT "simple"; IDENT"destruct"; h = quantified_hypothesis ->
           TacSimpleDestruct h
-      | IDENT "destruct"; c = induction_arg; ids = with_names;
-	  el = OPT eliminator -> TacNewDestruct (c,el,ids)
+      | IDENT "destruct"; c = induction_arg; ids = with_names; 
+	  el = OPT eliminator -> TacNewDestruct (c,el,(ids,ref []))
       | IDENT "decompose"; IDENT "record" ; c = constr -> TacDecomposeAnd c
       | IDENT "decompose"; IDENT "sum"; c = constr -> TacDecomposeOr c
       | IDENT "decompose"; "["; l = LIST1 global; "]"; c = constr
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index d7b2cbe449..8a97eb2d0f 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -477,14 +477,14 @@ and pr_atom1 = function
       hov 1 (str "Instantiate" ++ pr_arg int n ++ pr_arg pr_constr c ++ 
 	     pr_clauses pr_ident cls)
   (* Derived basic tactics *)
-  | TacSimpleInduction h ->
+  | TacSimpleInduction (h,_) ->
       hov 1 (str "Induction" ++ pr_arg pr_quantified_hypothesis h)
-  | TacNewInduction (h,e,ids) ->
+  | TacNewInduction (h,e,(ids,_)) ->
       hov 1 (str "NewInduction" ++ spc () ++ pr_induction_arg pr_constr h ++
         pr_opt pr_eliminator e ++ pr_with_names ids)
   | TacSimpleDestruct h ->
       hov 1 (str "Destruct" ++ pr_arg pr_quantified_hypothesis h)
-  | TacNewDestruct (h,e,ids) ->
+  | TacNewDestruct (h,e,(ids,_)) ->
       hov 1 (str "NewDestruct" ++ spc () ++ pr_induction_arg pr_constr h ++
         pr_opt pr_eliminator e ++ pr_with_names ids)
   | TacDoubleInduction (h1,h2) ->
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 57ca81de38..84efdbcac1 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -389,18 +389,18 @@ let rec mlexpr_of_atomic_tactic = function
       <:expr< Tacexpr.TacLetTac $id$ $mlexpr_of_constr c$ $cl$ >>
 
   (* Derived basic tactics *)
-  | Tacexpr.TacSimpleInduction h ->
-      <:expr< Tacexpr.TacSimpleInduction $mlexpr_of_quantified_hypothesis h$ >>
+  | Tacexpr.TacSimpleInduction (h,_) ->
+      <:expr< Tacexpr.TacSimpleInduction ($mlexpr_of_quantified_hypothesis h$,ref []) >>
   | Tacexpr.TacNewInduction (c,cbo,ids) ->
       let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
-      let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_intro_pattern) ids in
-      <:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ $cbo$ $ids$>>
+      let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_intro_pattern) (fst ids) in
+      <:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ $cbo$ ($ids$,ref [])>>
   | Tacexpr.TacSimpleDestruct h ->
       <:expr< Tacexpr.TacSimpleDestruct $mlexpr_of_quantified_hypothesis h$ >>
   | Tacexpr.TacNewDestruct (c,cbo,ids) ->
       let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
-      let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_intro_pattern) ids in
-      <:expr< Tacexpr.TacNewDestruct $mlexpr_of_induction_arg c$ $cbo$ $ids$ >>
+      let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_intro_pattern) (fst ids) in
+      <:expr< Tacexpr.TacNewDestruct $mlexpr_of_induction_arg c$ $cbo$ ($ids$,ref []) >>
 
   (* Context management *)
   | Tacexpr.TacClear l ->