Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id variable de ltac substituable dans la pratique par un intro_case_pattern dans induction, destruct et inversion

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

8 files changed, 36 insertions, 34 deletions

diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index cff5dccdeb..7c8c1b3c56 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -58,11 +58,11 @@ val h_simple_induction   : quantified_hypothesis * (bool ref * intro_pattern_exp
 val h_simple_destruct    : quantified_hypothesis -> tactic
 val h_new_induction   :
   constr induction_arg -> constr with_bindings option ->
-  case_intro_pattern_expr * (bool ref * intro_pattern_expr list ref list) list ref
+  intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref
   -> tactic
 val h_new_destruct    :
   constr induction_arg -> constr with_bindings option -> 
-  case_intro_pattern_expr * (bool ref * intro_pattern_expr list ref list) list ref
+  intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref
   -> tactic
 val h_specialize      : int option -> constr with_bindings -> tactic
 val h_lapply          : constr -> tactic
diff --git a/tactics/inv.ml b/tactics/inv.ml
index b9574db237..0810caa82a 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -523,15 +523,15 @@ open Tacexpr
 
 let inv k = inv_gen false k NoDep
 
-let half_inv_tac id  = inv SimpleInversion [] (NamedHyp id)
-let inv_tac id       = inv FullInversion [] (NamedHyp id)
-let inv_clear_tac id = inv FullInversionClear [] (NamedHyp id)
+let half_inv_tac id  = inv SimpleInversion None (NamedHyp id)
+let inv_tac id       = inv FullInversion None (NamedHyp id)
+let inv_clear_tac id = inv FullInversionClear None (NamedHyp id)
 
 let dinv k c = inv_gen false k (Dep c)
 
-let half_dinv_tac id  = dinv SimpleInversion None [] (NamedHyp id)
-let dinv_tac id       = dinv FullInversion None [] (NamedHyp id)
-let dinv_clear_tac id = dinv FullInversionClear None [] (NamedHyp id)
+let half_dinv_tac id  = dinv SimpleInversion None None (NamedHyp id)
+let dinv_tac id       = dinv FullInversion None None (NamedHyp id)
+let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id)
 
 (* InvIn will bring the specified clauses into the conclusion, and then
  * perform inversion on the named hypothesis.  After, it will intro them
diff --git a/tactics/inv.mli b/tactics/inv.mli
index 4c3cb00f82..95bf4c6f7b 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -21,19 +21,19 @@ type inversion_status = Dep of constr option | NoDep
 
 val inv_gen :
   bool -> inversion_kind -> inversion_status ->
-    case_intro_pattern_expr -> quantified_hypothesis -> tactic
+    intro_pattern_expr option -> quantified_hypothesis -> tactic
 val invIn_gen :
-  inversion_kind -> case_intro_pattern_expr -> identifier list -> 
+  inversion_kind -> intro_pattern_expr option -> identifier list -> 
     quantified_hypothesis -> tactic
 
 val inv_clause :
-  inversion_kind -> case_intro_pattern_expr -> identifier list ->
+  inversion_kind -> intro_pattern_expr option -> identifier list ->
     quantified_hypothesis -> tactic
 
-val inv : inversion_kind -> case_intro_pattern_expr ->
+val inv : inversion_kind -> intro_pattern_expr option ->
   quantified_hypothesis -> tactic
 
-val dinv : inversion_kind -> constr option -> case_intro_pattern_expr ->
+val dinv : inversion_kind -> constr option -> intro_pattern_expr option ->
   quantified_hypothesis -> tactic
 
 val half_inv_tac : identifier -> tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a0d791a58b..4a08804c5a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -549,10 +549,10 @@ let intern_redexp ist = function
 let intern_inversion_strength lf ist = function
   | NonDepInversion (k,idl,ids) ->
       NonDepInversion (k,List.map (intern_hyp_or_metaid ist) idl,
-      intern_case_intro_pattern lf ist ids)
+      option_app (intern_intro_pattern lf ist) ids)
   | DepInversion (k,copt,ids) ->
       DepInversion (k, option_app (intern_constr ist) copt,
-      intern_case_intro_pattern lf ist ids)
+      option_app (intern_intro_pattern lf ist) ids)
   | InversionUsing (c,idl) ->
       InversionUsing (intern_constr ist c, List.map (intern_hyp_or_metaid ist) idl)
 
@@ -672,13 +672,13 @@ let rec intern_atomic lf ist x =
   | TacNewInduction (c,cbo,(ids,ids')) ->
       TacNewInduction (intern_induction_arg ist c,
                option_app (intern_constr_with_bindings ist) cbo,
-               (intern_case_intro_pattern lf ist ids,ids'))
+               (option_app (intern_intro_pattern lf ist) ids,ids'))
   | TacSimpleDestruct h ->
       TacSimpleDestruct (intern_quantified_hypothesis ist h)
   | TacNewDestruct (c,cbo,(ids,ids')) ->
       TacNewDestruct (intern_induction_arg ist c,
                option_app (intern_constr_with_bindings ist) cbo,
-	       (intern_case_intro_pattern lf ist ids,ids'))
+	       (option_app (intern_intro_pattern lf ist) ids,ids'))
   | TacDoubleInduction (h1,h2) ->
       let h1 = intern_quantified_hypothesis ist h1 in
       let h2 = intern_quantified_hypothesis ist h2 in
@@ -1704,13 +1704,13 @@ and interp_atomic ist gl = function
   | TacNewInduction (c,cbo,(ids,ids')) ->
       h_new_induction (interp_induction_arg ist gl c)
         (option_app (interp_constr_with_bindings ist gl) cbo)
-        (interp_case_intro_pattern ist ids,ids')
+        (option_app (interp_intro_pattern ist) ids,ids')
   | TacSimpleDestruct h ->
       h_simple_destruct (interp_quantified_hypothesis ist gl h)
   | TacNewDestruct (c,cbo,(ids,ids')) -> 
       h_new_destruct (interp_induction_arg ist gl c)
         (option_app (interp_constr_with_bindings ist gl) cbo)
-        (interp_case_intro_pattern ist ids,ids')
+        (option_app (interp_intro_pattern ist) ids,ids')
   | TacDoubleInduction (h1,h2) ->
       let h1 = interp_quantified_hypothesis ist gl h1 in
       let h2 = interp_quantified_hypothesis ist gl h2 in
@@ -1757,11 +1757,11 @@ and interp_atomic ist gl = function
   (* Equality and inversion *)
   | TacInversion (DepInversion (k,c,ids),hyp) ->
       Inv.dinv k (option_app (pf_interp_constr ist gl) c)
-        (interp_case_intro_pattern ist ids)
+        (option_app (interp_intro_pattern ist) ids)
         (interp_quantified_hypothesis ist gl hyp)
   | TacInversion (NonDepInversion (k,idl,ids),hyp) ->
       Inv.inv_clause k 
-        (interp_case_intro_pattern ist ids)
+        (option_app (interp_intro_pattern ist) ids)
         (List.map (interp_hyp ist gl) idl)
         (interp_quantified_hypothesis ist gl hyp)
   | TacInversion (InversionUsing (c,idl),hyp) ->
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index bd75581aae..7dc71ffc96 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -267,11 +267,13 @@ type branch_assumptions = {
   ba        : branch_args;     (* the branch args *)
   assums    : named_context}   (* the list of assumptions introduced *)
 
-let compute_induction_names n names =
-  let names = if names = [] then Array.make n [] else Array.of_list names in
-  if Array.length names <> n then
-    errorlabstrm "" (str "Expects " ++ int n ++ str " lists of names");
-  names
+let compute_induction_names n = function
+  | None ->
+      Array.make n []
+  | Some (IntroOrAndPattern names) when List.length names = n ->
+      Array.of_list names
+  | _ ->
+      errorlabstrm "" (str "Expects " ++ int n ++ str " lists of names")
 
 let compute_construtor_signatures isrec (_,k as ity) =
   let rec analrec c recargs =
@@ -377,7 +379,7 @@ let elimination_then_using tac predicate (indbindings,elimbindings) c gl =
   let elim =
     Indrec.lookup_eliminator ind (elimination_sort_of_goal gl) in
   general_elim_then_using
-    elim true [] tac predicate (indbindings,elimbindings) c gl
+    elim true None tac predicate (indbindings,elimbindings) c gl
 
 
 let elimination_then tac        = elimination_then_using tac None 
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index f6b6e5b001..1a6a540e61 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -129,13 +129,13 @@ type branch_assumptions = {
 
 (* Useful for "as intro_pattern" modifier *)
 val compute_induction_names : 
-  int -> case_intro_pattern_expr -> intro_pattern_expr list array
+  int -> intro_pattern_expr option -> intro_pattern_expr list array
 
 val elimination_sort_of_goal : goal sigma -> sorts_family
 val elimination_sort_of_hyp  : identifier -> goal sigma -> sorts_family
 
 val general_elim_then_using :
-  constr -> (* isrec: *) bool -> case_intro_pattern_expr ->
+  constr -> (* isrec: *) bool -> intro_pattern_expr option ->
     (branch_args -> tactic) -> constr option -> 
       (arg_bindings * arg_bindings) -> constr -> tactic
 	  
@@ -148,11 +148,11 @@ val elimination_then :
     (arg_bindings * arg_bindings) -> constr -> tactic
 
 val case_then_using :
-  case_intro_pattern_expr -> (branch_args -> tactic) -> 
+  intro_pattern_expr option -> (branch_args -> tactic) -> 
     constr option -> (arg_bindings * arg_bindings) -> constr -> tactic
 
 val case_nodep_then_using :
-  case_intro_pattern_expr -> (branch_args -> tactic) -> 
+  intro_pattern_expr option -> (branch_args -> tactic) -> 
     constr option -> (arg_bindings * arg_bindings) -> constr -> tactic
 
 val simple_elimination_then :
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6444c1756b..c069fc1f5f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1639,7 +1639,7 @@ let raw_induct_nodep n = tclTHEN (intros_until_n n) (tclLAST_HYP simplest_elim)
 (* This was Induction in 6.3 (hybrid form) *)
 let induction_from_context_old_style hyp b_ids gl =
   let elim_info = find_elim_signature true true None hyp gl in
-  let x = induction_from_context true elim_info hyp ([],b_ids) gl in
+  let x = induction_from_context true elim_info hyp (None,b_ids) gl in
   (* For translator *) fst (List.hd !b_ids) := true;
   x
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index b33bc52f0e..a12404a9a4 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -177,7 +177,7 @@ val general_elim_in : identifier -> constr * constr bindings ->
                       constr * constr bindings -> tactic
 
 val new_induct : constr induction_arg -> constr with_bindings option ->
-  case_intro_pattern_expr * (bool ref * intro_pattern_expr list ref list) list ref
+  intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref
   -> tactic
 
 (*s Case analysis tactics. *)
@@ -187,7 +187,7 @@ val simplest_case         : constr -> tactic
 
 val simple_destruct          : quantified_hypothesis -> tactic
 val new_destruct : constr induction_arg -> constr with_bindings option ->
-  case_intro_pattern_expr * (bool ref * intro_pattern_expr list ref list) list ref
+  intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref
   -> tactic
 
 (*s Eliminations giving the type instead of the proof. *)