Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq

choisir un nom; utilisation de IntroAnonymous au lieu de None dans
l'argument "with_names" des tactiques induction, inversion et assert.


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

8 files changed, 86 insertions, 83 deletions

diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 3e66391cfc..6470b7a24d 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -58,10 +58,10 @@ val h_simple_induction   : quantified_hypothesis -> tactic
 val h_simple_destruct    : quantified_hypothesis -> tactic
 val h_new_induction   :
   constr induction_arg -> constr with_bindings option ->
-  intro_pattern_expr option -> tactic
+  intro_pattern_expr -> tactic
 val h_new_destruct    :
   constr induction_arg -> constr with_bindings option -> 
-  intro_pattern_expr option -> tactic
+  intro_pattern_expr -> 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 9597cfa41f..b799c939f8 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -377,6 +377,8 @@ let rewrite_equations_gene othin neqns ba gl =
 let rec get_names allow_conj = function
   | IntroWildcard ->
       error "Discarding pattern not allowed for inversion equations"
+  | IntroAnonymous ->
+      error "Anonymous pattern not allowed for inversion equations"
   | IntroOrAndPattern [l] -> 
       if allow_conj then
 	if l = [] then (None,[]) else
@@ -519,15 +521,15 @@ open Tacexpr
 
 let inv k = inv_gen false k NoDep
 
-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 half_inv_tac id  = inv SimpleInversion IntroAnonymous (NamedHyp id)
+let inv_tac id       = inv FullInversion IntroAnonymous (NamedHyp id)
+let inv_clear_tac id = inv FullInversionClear IntroAnonymous (NamedHyp id)
 
 let dinv k c = inv_gen false k (Dep c)
 
-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)
+let half_dinv_tac id  = dinv SimpleInversion None IntroAnonymous (NamedHyp id)
+let dinv_tac id       = dinv FullInversion None IntroAnonymous (NamedHyp id)
+let dinv_clear_tac id = dinv FullInversionClear None IntroAnonymous (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 7f80a03357..086c9d7cea 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 ->
-    intro_pattern_expr option -> quantified_hypothesis -> tactic
+    intro_pattern_expr -> quantified_hypothesis -> tactic
 val invIn_gen :
-  inversion_kind -> intro_pattern_expr option -> identifier list -> 
+  inversion_kind -> intro_pattern_expr -> identifier list -> 
     quantified_hypothesis -> tactic
 
 val inv_clause :
-  inversion_kind -> intro_pattern_expr option -> identifier list ->
+  inversion_kind -> intro_pattern_expr -> identifier list ->
     quantified_hypothesis -> tactic
 
-val inv : inversion_kind -> intro_pattern_expr option ->
+val inv : inversion_kind -> intro_pattern_expr ->
   quantified_hypothesis -> tactic
 
-val dinv : inversion_kind -> constr option -> intro_pattern_expr option ->
+val dinv : inversion_kind -> constr option -> intro_pattern_expr ->
   quantified_hypothesis -> tactic
 
 val half_inv_tac : identifier -> tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index c3c01f3a2f..d1bf4389d9 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -417,10 +417,9 @@ let intern_reference strict ist r =
 let rec intern_intro_pattern lf ist = function
   | IntroOrAndPattern l ->
       IntroOrAndPattern (intern_case_intro_pattern lf ist l)
-  | IntroWildcard ->
-      IntroWildcard
   | IntroIdentifier id ->
       IntroIdentifier (intern_ident lf ist id)
+  | IntroWildcard | IntroAnonymous as x -> x
 
 and intern_case_intro_pattern lf ist =
   List.map (List.map (intern_intro_pattern lf ist))
@@ -513,10 +512,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,
-      option_app (intern_intro_pattern lf ist) ids)
+      intern_intro_pattern lf ist ids)
   | DepInversion (k,copt,ids) ->
       DepInversion (k, option_app (intern_constr ist) copt,
-      option_app (intern_intro_pattern lf ist) ids)
+      intern_intro_pattern lf ist ids)
   | InversionUsing (c,idl) ->
       InversionUsing (intern_constr ist c, List.map (intern_hyp_or_metaid ist) idl)
 
@@ -633,7 +632,7 @@ let rec intern_atomic lf ist x =
   | TacCut c -> TacCut (intern_type ist c)
   | TacAssert (otac,ipat,c) ->
       TacAssert (option_app (intern_tactic ist) otac,
-                 option_app (intern_intro_pattern lf ist) ipat,
+                 intern_intro_pattern lf ist ipat,
                  intern_constr_gen (otac<>None) ist c)
   | TacGeneralize cl -> TacGeneralize (List.map (intern_constr ist) cl)
   | TacGeneralizeDep c -> TacGeneralizeDep (intern_constr ist c)
@@ -664,13 +663,13 @@ let rec intern_atomic lf ist x =
   | TacNewInduction (c,cbo,ids) ->
       TacNewInduction (intern_induction_arg ist c,
                option_app (intern_constr_with_bindings ist) cbo,
-               (option_app (intern_intro_pattern lf ist) ids))
+               (intern_intro_pattern lf ist ids))
   | TacSimpleDestruct h ->
       TacSimpleDestruct (intern_quantified_hypothesis ist h)
   | TacNewDestruct (c,cbo,ids) ->
       TacNewDestruct (intern_induction_arg ist c,
                option_app (intern_constr_with_bindings ist) cbo,
-	       (option_app (intern_intro_pattern lf ist) ids))
+	       (intern_intro_pattern lf ist ids))
   | TacDoubleInduction (h1,h2) ->
       let h1 = intern_quantified_hypothesis ist h1 in
       let h2 = intern_quantified_hypothesis ist h2 in
@@ -1138,7 +1137,7 @@ let rec intropattern_ids = function
   | IntroIdentifier id -> [id]
   | IntroOrAndPattern ll -> 
       List.flatten (List.map intropattern_ids (List.flatten ll))
-  | IntroWildcard -> []
+  | IntroWildcard | IntroAnonymous -> []
 
 let rec extract_ids = function
   | (id,VIntroPattern ipat)::tl -> intropattern_ids ipat @ extract_ids tl
@@ -1290,8 +1289,8 @@ let interp_constr_may_eval ist gl c =
 
 let rec interp_intro_pattern ist = function
   | IntroOrAndPattern l -> IntroOrAndPattern (interp_case_intro_pattern ist l)
-  | IntroWildcard -> IntroWildcard
   | IntroIdentifier id -> interp_intro_pattern_var ist id
+  | IntroWildcard | IntroAnonymous as x -> x
 
 and interp_case_intro_pattern ist =
   List.map (List.map (interp_intro_pattern ist))
@@ -1707,7 +1706,7 @@ and interp_atomic ist gl = function
       let c = (if t=None then pf_interp_constr else pf_interp_type) ist gl c in
       abstract_tactic (TacAssert (t,ipat,c))
         (Tactics.forward (option_app (interp_tactic ist) t)
-	  (option_app (interp_intro_pattern ist) ipat) c)
+	  (interp_intro_pattern ist ipat) c)
   | TacGeneralize cl -> h_generalize (List.map (pf_interp_constr ist gl) cl)
   | TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c)
   | TacLetTac (na,c,clp) ->
@@ -1737,13 +1736,13 @@ and interp_atomic ist gl = function
   | TacNewInduction (c,cbo,ids) ->
       h_new_induction (interp_induction_arg ist gl c)
         (option_app (interp_constr_with_bindings ist gl) cbo)
-        (option_app (interp_intro_pattern ist) ids)
+        (interp_intro_pattern ist ids)
   | TacSimpleDestruct h ->
       h_simple_destruct (interp_quantified_hypothesis ist h)
   | TacNewDestruct (c,cbo,ids) -> 
       h_new_destruct (interp_induction_arg ist gl c)
         (option_app (interp_constr_with_bindings ist gl) cbo)
-        (option_app (interp_intro_pattern ist) ids)
+        (interp_intro_pattern ist ids)
   | TacDoubleInduction (h1,h2) ->
       let h1 = interp_quantified_hypothesis ist h1 in
       let h2 = interp_quantified_hypothesis ist h2 in
@@ -1790,11 +1789,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)
-        (option_app (interp_intro_pattern ist) ids)
+        (interp_intro_pattern ist ids)
         (interp_declared_or_quantified_hypothesis ist gl hyp)
   | TacInversion (NonDepInversion (k,idl,ids),hyp) ->
       Inv.inv_clause k 
-        (option_app (interp_intro_pattern ist) ids)
+        (interp_intro_pattern ist ids)
         (List.map (interp_hyp ist gl) idl)
         (interp_declared_or_quantified_hypothesis ist gl hyp)
   | TacInversion (InversionUsing (c,idl),hyp) ->
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 05eb17fe7b..517d774d4d 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -266,9 +266,9 @@ type branch_assumptions = {
   assums    : named_context}   (* the list of assumptions introduced *)
 
 let compute_induction_names n = function
-  | None ->
+  | IntroAnonymous ->
       Array.make n []
-  | Some (IntroOrAndPattern names) when List.length names = n ->
+  | IntroOrAndPattern names when List.length names = n ->
       Array.of_list names
   | _ ->
       errorlabstrm "" (str "Expects " ++ int n ++ str " lists of names")
@@ -377,7 +377,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 None tac predicate (indbindings,elimbindings) c gl
+    elim true IntroAnonymous 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 67dbcfc0f4..699c0d7801 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 -> intro_pattern_expr option -> intro_pattern_expr list array
+  int -> intro_pattern_expr -> 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 -> intro_pattern_expr option ->
+  constr -> (* isrec: *) bool -> intro_pattern_expr ->
     (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 :
-  intro_pattern_expr option -> (branch_args -> tactic) -> 
+  intro_pattern_expr -> (branch_args -> tactic) -> 
     constr option -> (arg_bindings * arg_bindings) -> constr -> tactic
 
 val case_nodep_then_using :
-  intro_pattern_expr option -> (branch_args -> tactic) -> 
+  intro_pattern_expr -> (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 b277df0e00..36b948862a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -798,7 +798,7 @@ let clear_last = tclLAST_HYP (fun c -> (clear [destVar c]))
 let case_last  = tclLAST_HYP simplest_case
 
 let rec explicit_intro_names = function
-| IntroWildcard :: l -> explicit_intro_names l
+| (IntroWildcard | IntroAnonymous) :: l -> explicit_intro_names l
 | IntroIdentifier id :: l -> id :: explicit_intro_names l
 | IntroOrAndPattern ll :: l' -> 
     List.flatten (List.map (fun l -> explicit_intro_names (l@l')) ll)
@@ -808,26 +808,33 @@ let rec explicit_intro_names = function
      to ensure that dependent hypotheses are cleared in the right
      dependency order (see bug #1000); we use fresh names, not used in
      the tactic, for the hyps to clear *)
-let rec intros_patterns thin destopt = function
+let rec intros_patterns avoid thin destopt = function
   | IntroWildcard :: l ->
       tclTHEN 
-        (intro_gen (IntroAvoid (explicit_intro_names l)) None true)
-        (onLastHyp (fun id -> intros_patterns (id::thin) destopt l))
+        (intro_gen (IntroAvoid (avoid@explicit_intro_names l)) None true)
+        (onLastHyp (fun id ->
+	  tclORELSE
+	    (tclTHEN (clear [id]) (intros_patterns avoid thin destopt l))
+	    (intros_patterns avoid (id::thin) destopt l)))
   | IntroIdentifier id :: l ->
       tclTHEN
         (intro_gen (IntroMustBe id) destopt true)
-        (intros_patterns thin destopt l)
+        (intros_patterns avoid thin destopt l)
+  | IntroAnonymous :: l ->
+      tclTHEN
+        (intro_gen (IntroAvoid (avoid@explicit_intro_names l)) destopt true)
+        (intros_patterns avoid thin destopt l)
   | IntroOrAndPattern ll :: l' ->
       tclTHEN
         introf
         (tclTHENS
 	  (tclTHEN case_last clear_last)
-	  (List.map (fun l -> intros_patterns thin destopt (l@l')) ll))
+	  (List.map (fun l -> intros_patterns avoid thin destopt (l@l')) ll))
   | [] -> clear thin
 
-let intros_pattern = intros_patterns []
+let intros_pattern = intros_patterns [] []
 
-let intro_pattern destopt pat = intros_patterns [] destopt [pat]
+let intro_pattern destopt pat = intros_patterns [] [] destopt [pat]
 
 let intro_patterns = function 
   | [] -> tclREPEAT intro
@@ -843,17 +850,17 @@ let xid = id_of_string "X"
 let make_id s = fresh_id [] (match s with Prop _ -> hid | Type _ -> xid)
 
 let prepare_intros s ipat gl = match ipat with
-  | None -> make_id s gl, tclIDTAC
-  | Some IntroWildcard -> let id = make_id s gl in id, thin [id]
-  | Some (IntroIdentifier id) -> id, tclIDTAC
-  | Some (IntroOrAndPattern ll) -> make_id s gl, 
-        (tclTHENS 
-	  (tclTHEN case_last clear_last)
-	  (List.map (intros_patterns [] None) ll))
+  | IntroAnonymous -> make_id s gl, tclIDTAC
+  | IntroWildcard -> let id = make_id s gl in id, thin [id]
+  | IntroIdentifier id -> id, tclIDTAC
+  | IntroOrAndPattern ll -> make_id s gl, 
+    (tclTHENS 
+      (tclTHEN case_last clear_last)
+      (List.map (intros_pattern None) ll))
 
 let ipat_of_name = function
-  | Anonymous -> None
-  | Name id -> Some (IntroIdentifier id)
+  | Anonymous -> IntroAnonymous
+  | Name id -> IntroIdentifier id
 
 let assert_as first ipat c gl =
   match kind_of_term (hnf_type_of gl c) with
@@ -1124,6 +1131,14 @@ let rec first_name_buggy = function
   | IntroOrAndPattern ((p::_)::_) -> first_name_buggy p
   | IntroWildcard -> None
   | IntroIdentifier id -> Some id
+  | IntroAnonymous -> assert false
+
+let consume_pattern avoid id gl = function
+  | [] -> (IntroIdentifier (fresh_id avoid id gl), [])
+  | IntroAnonymous::names ->
+      let avoid = avoid@explicit_intro_names names in
+      (IntroIdentifier (fresh_id avoid id gl), names)
+  | pat::names -> (pat,names)
 
 type elim_arg_kind = RecArg | IndArg | OtherArg
 
@@ -1134,43 +1149,30 @@ let induct_discharge statuslists destopt avoid' (avoid,ra) names gl =
   let rec peel_tac ra names gl = match ra with
     | (RecArg,recvarname) ::
         (IndArg,hyprecname) :: ra' ->
-        let recpat,hyprec,names = match names with
-          | [] ->
-              let idrec = fresh_id avoid recvarname gl in
-              let idhyp = fresh_id avoid hyprecname gl in
-              (IntroIdentifier idrec, IntroIdentifier idhyp, [])
+        let recpat,names = match names with
           | [IntroIdentifier id as pat] ->
               let id = next_ident_away (add_prefix "IH" id) avoid in
-	      (pat, IntroIdentifier id, [])
-	  | [pat] ->
-              let idhyp = (fresh_id avoid hyprecname gl) in
-	      (pat, IntroIdentifier idhyp, [])
-          | pat1::pat2::names -> (pat1,pat2,names) in
+	      (pat, [IntroIdentifier id])
+          | _ -> consume_pattern avoid recvarname gl names in
+        let hyprec,names = consume_pattern avoid hyprecname gl names in
 	(* This is buggy for intro-or-patterns with different first hypnames *)
 	if !tophyp=None then tophyp := first_name_buggy hyprec;
         tclTHENLIST
-	  [ intros_pattern destopt [recpat];
-	    intros_pattern None [hyprec];
+	  [ intros_patterns avoid [] destopt [recpat];
+	    intros_patterns avoid [] None [hyprec];
 	    peel_tac ra' names ] gl
     | (IndArg,hyprecname) :: ra' ->
 	(* Rem: does not happen in Coq schemes, only in user-defined schemes *)
-        let pat,names = match names with
-          | [] -> IntroIdentifier (fresh_id avoid hyprecname gl), []
-	  | pat::names -> pat,names in
-	tclTHEN (intros_pattern destopt [pat]) (peel_tac ra' names) gl
+        let pat,names = consume_pattern avoid hyprecname gl names in
+	tclTHEN (intros_patterns avoid [] destopt [pat]) (peel_tac ra' names) gl
     | (RecArg,recvarname) :: ra' ->
-        let introtac,names = match names with
-          | [] -> 
-              let id = fresh_id avoid recvarname gl in
-	      intro_gen (IntroMustBe id) destopt false, []
-          | pat::names ->
-	      intros_pattern destopt [pat],names in
-	tclTHEN introtac (peel_tac ra' names) gl
+        let pat,names = consume_pattern avoid recvarname gl names in
+	tclTHEN (intros_patterns avoid [] destopt [pat]) (peel_tac ra' names) gl
     | (OtherArg,_) :: ra' ->
-        let introtac,names = match names with
-          | [] -> intro_gen (IntroAvoid avoid) destopt false, []
-          | pat::names -> intros_pattern destopt [pat],names in
-	tclTHEN introtac (peel_tac ra' names) gl
+        let pat,names = match names with
+          | [] -> IntroAnonymous, []
+          | pat::names -> pat,names in
+	tclTHEN (intros_patterns avoid [] destopt [pat]) (peel_tac ra' names) gl
     | [] ->
         check_unused_names names;
         tclIDTAC gl
@@ -1491,7 +1493,6 @@ let induction_from_context isrec elim_info hyp0 names gl =
   let (statlists,lhyp0,indhyps,deps) = cook_sign hyp0 indvars env in
   let tmpcl = it_mkNamedProd_or_LetIn (pf_concl gl) deps in
   let names = compute_induction_names (Array.length indsign) names in
-  (* End translator *)
   let dephyps = List.map (fun (id,_,_) -> id) deps in
   let args =
     List.fold_left
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 95a2facc07..cf0b06862e 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -178,7 +178,7 @@ val elim          : constr with_bindings -> constr with_bindings option -> tacti
 val simple_induct : quantified_hypothesis -> tactic
 
 val new_induct : constr induction_arg -> constr with_bindings option ->
-  intro_pattern_expr option -> tactic
+  intro_pattern_expr -> 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 ->
-  intro_pattern_expr option -> tactic
+  intro_pattern_expr -> tactic
 
 (*s Eliminations giving the type instead of the proof. *)
 
@@ -239,11 +239,12 @@ val cut_replacing               :
   identifier -> constr -> (tactic -> tactic) -> tactic
 val cut_in_parallel             : constr list -> tactic
 
-val assert_as : bool -> intro_pattern_expr option -> constr -> tactic
+val assert_as : bool -> intro_pattern_expr -> constr -> tactic
+val forward   : tactic option -> intro_pattern_expr -> constr -> tactic
+
 val true_cut                    : name -> constr -> tactic
 val letin_tac                   : bool -> name -> constr -> clause -> tactic
 val assert_tac                  : bool -> name -> constr -> tactic
-val forward    : tactic option -> intro_pattern_expr option -> constr -> tactic
 val generalize                  : constr list -> tactic
 val generalize_dep              : constr  -> tactic