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

10 files changed, 22 insertions, 5 deletions

diff --git a/CHANGES b/CHANGES
index 18a522f7ab..fb7c018563 100644
--- a/CHANGES
+++ b/CHANGES
@@ -56,6 +56,7 @@ Tactics
 - The "with" arguments are now typed using informations from the current goal:
   allows support for coercions and more inference of implicit arguments.
 - Application of "f_equal"-style lemmas works better.
+- New intro pattern "@A", which genererates a fresh name based on A.
 
 Miscellaneous
 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index fe1c55003e..202e58472e 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -632,6 +632,7 @@ let rec xlate_intro_pattern =
   | IntroWildcard -> CT_coerce_ID_to_INTRO_PATT(CT_ident "_" )
   | IntroIdentifier c -> CT_coerce_ID_to_INTRO_PATT(xlate_ident c)
   | IntroAnonymous -> xlate_error "TODO: IntroAnonymous"
+  | IntroFresh _ -> xlate_error "TODO: IntroFresh"
 
 let compute_INV_TYPE = function
    FullInversionClear -> CT_inv_clear
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index dc2f65a152..d04d8e3134 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1442,6 +1442,7 @@ An introduction pattern is either:
 \begin{itemize}
 \item the wildcard: {\tt \_}
 \item the pattern \texttt{?}
+\item the pattern \texttt{@\ident}
 \item a variable
 \item a disjunction of lists of patterns:
   {\tt [$p_{11}$ {\ldots} $p_{1m_1}$ | {\ldots} | $p_{11}$ {\ldots} $p_{nm_n}$]}
@@ -1455,6 +1456,8 @@ structure of the pattern given as argument:
   immediately clear (cf~\ref{clear}) the corresponding hypothesis;
 \item introduction on \texttt{?} do the introduction, and let Coq
   choose a fresh name for the variable;
+\item introduction on \texttt{@\ident} do the introduction, and let Coq
+  choose a fresh name for the variable based on {\ident};
 \item introduction on a variable behaves like described in~\ref{intro}; 
 \item introduction over a
 list of patterns $p_1~\ldots~p_n$ is equivalent to the sequence of
diff --git a/interp/genarg.ml b/interp/genarg.ml
index d98788eede..2c61fc3c9b 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -79,6 +79,7 @@ type intro_pattern_expr =
   | IntroWildcard
   | IntroIdentifier of identifier
   | IntroAnonymous
+  | IntroFresh of identifier
 and case_intro_pattern_expr = intro_pattern_expr list list
 
 let rec pr_intro_pattern = function
@@ -86,6 +87,7 @@ let rec pr_intro_pattern = function
   | IntroWildcard -> str "_"
   | IntroIdentifier id -> pr_id id
   | IntroAnonymous -> str "?"
+  | IntroFresh id -> str "@" ++ pr_id id
 
 and pr_case_intro_pattern = function
   | [pl] ->
diff --git a/interp/genarg.mli b/interp/genarg.mli
index ccaf93d58c..0df4e66a01 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -36,6 +36,7 @@ type intro_pattern_expr =
   | IntroWildcard
   | IntroIdentifier of identifier
   | IntroAnonymous
+  | IntroFresh of identifier
 and case_intro_pattern_expr = intro_pattern_expr list list
 
 val pr_intro_pattern : intro_pattern_expr -> Pp.std_ppcmds
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index a15a6c12df..9f783771b7 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -186,6 +186,7 @@ GEXTEND Gram
 	    | t::q -> IntroOrAndPattern [[t;pairify q]]
 	  in pairify tc
       | "_" -> IntroWildcard
+      | "@"; prefix = ident -> IntroFresh prefix
       | "?" -> IntroAnonymous
       | id = ident -> IntroIdentifier id
       ] ]
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index a8c975eb1f..331fbdd989 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -63,6 +63,7 @@ let mlexpr_of_intro_pattern = function
   | Genarg.IntroOrAndPattern _ -> failwith "mlexpr_of_intro_pattern: TODO"
   | Genarg.IntroWildcard -> <:expr< Genarg.IntroWildcard >>
   | Genarg.IntroAnonymous -> <:expr< Genarg.IntroAnonymous >>
+  | Genarg.IntroFresh id -> <:expr< Genarg.IntroFresh (mlexpr_of_ident $dloc$ id) >>
   | Genarg.IntroIdentifier id ->
       <:expr< Genarg.IntroIdentifier (mlexpr_of_ident $dloc$ id) >>
 
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), [])