New intro pattern "@A", which generates a fresh name based on A.

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

3 files changed, 12 insertions, 5 deletions

diff --git a/tactics/inv.ml b/tactics/inv.ml
index 6a9dc632b5..daa6e27779 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -379,6 +379,8 @@ let rec get_names allow_conj = function
       error "Discarding pattern not allowed for inversion equations"
   | IntroAnonymous ->
       error "Anonymous pattern not allowed for inversion equations"
+  | IntroFresh _->
+      error "Fresh pattern not allowed for inversion equations"
   | IntroOrAndPattern [l] -> 
       if allow_conj then
 	if l = [] then (None,[]) else
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index aba013c1c1..d52093230d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -443,7 +443,7 @@ let rec intern_intro_pattern lf ist = function
       IntroOrAndPattern (intern_case_intro_pattern lf ist l)
   | IntroIdentifier id ->
       IntroIdentifier (intern_ident lf ist id)
-  | IntroWildcard | IntroAnonymous as x -> x
+  | IntroWildcard | IntroAnonymous | IntroFresh _ as x -> x
 
 and intern_case_intro_pattern lf ist =
   List.map (List.map (intern_intro_pattern lf ist))
@@ -1240,7 +1240,7 @@ let rec intropattern_ids = function
   | IntroIdentifier id -> [id]
   | IntroOrAndPattern ll -> 
       List.flatten (List.map intropattern_ids (List.flatten ll))
-  | IntroWildcard | IntroAnonymous -> []
+  | IntroWildcard | IntroAnonymous | IntroFresh _ -> []
 
 let rec extract_ids ids = function
   | (id,VIntroPattern ipat)::tl when not (List.mem id ids) ->
@@ -1492,7 +1492,7 @@ let rec interp_message_nl ist = function
 let rec interp_intro_pattern ist gl = function
   | IntroOrAndPattern l -> IntroOrAndPattern (interp_case_intro_pattern ist gl l)
   | IntroIdentifier id -> interp_intro_pattern_var ist (pf_env gl) id
-  | IntroWildcard | IntroAnonymous as x -> x
+  | IntroWildcard | IntroAnonymous | IntroFresh _ as x -> x
 
 and interp_case_intro_pattern ist gl =
   List.map (List.map (interp_intro_pattern ist gl))
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 99bb388365..ed5c7b1056 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -941,7 +941,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 | IntroAnonymous) :: l -> explicit_intro_names l
+| (IntroWildcard | IntroAnonymous | IntroFresh _) :: 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)
@@ -967,6 +967,10 @@ let rec intros_patterns avoid thin destopt = function
       tclTHEN
         (intro_gen (IntroAvoid (avoid@explicit_intro_names l)) destopt true)
         (intros_patterns avoid thin destopt l)
+  | IntroFresh id :: l ->
+      tclTHEN
+        (intro_gen (IntroBasedOn (id, avoid@explicit_intro_names l)) destopt true)
+        (intros_patterns avoid thin destopt l)
   | IntroOrAndPattern ll :: l' ->
       tclTHEN
         introf
@@ -994,6 +998,7 @@ let make_id s = fresh_id [] (match s with Prop _ -> hid | Type _ -> xid)
 
 let prepare_intros s ipat gl = match ipat with
   | IntroAnonymous -> make_id s gl, tclIDTAC
+  | IntroFresh id -> fresh_id [] id gl, tclIDTAC
   | IntroWildcard -> let id = make_id s gl in id, thin [id]
   | IntroIdentifier id -> id, tclIDTAC
   | IntroOrAndPattern ll -> make_id s gl, 
@@ -1305,7 +1310,7 @@ let rec first_name_buggy = function
   | IntroOrAndPattern ((p::_)::_) -> first_name_buggy p
   | IntroWildcard -> None
   | IntroIdentifier id -> Some id
-  | IntroAnonymous -> assert false
+  | IntroAnonymous | IntroFresh _ -> assert false
 
 let consume_pattern avoid id gl = function
   | [] -> (IntroIdentifier (fresh_id avoid id gl), [])