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

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

3 files changed, 5 insertions, 1 deletions

diff --git a/CHANGES b/CHANGES
index f6d9aac8a9..95ae28f45c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -59,6 +59,7 @@ Tactics
 - Low-priority term printer made available in ML-written tactic extensions
 - Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses
 - New tactic "pose proof" that generalizes "assert (id:=p)" with intro patterns
+- New introduction pattern "?" for letting Coq choose a name
 
 Modules
 
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 2646a4c825..385171fe35 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -69,15 +69,17 @@ type intro_pattern_expr =
   | IntroOrAndPattern of case_intro_pattern_expr
   | IntroWildcard
   | IntroIdentifier of identifier
+  | IntroAnonymous
 and case_intro_pattern_expr = intro_pattern_expr list list
 
 let rec pr_intro_pattern = function
   | IntroOrAndPattern pll -> pr_case_intro_pattern pll
   | IntroWildcard -> str "_"
   | IntroIdentifier id -> pr_id id
+  | IntroAnonymous -> str "?"
 
 and pr_case_intro_pattern = function
-  | [_::_ as pl] ->
+  | [pl] ->
       str "(" ++ hv 0 (prlist_with_sep pr_coma pr_intro_pattern pl) ++ str ")"
   | pll ->
       str "[" ++
diff --git a/interp/genarg.mli b/interp/genarg.mli
index d61245475c..858457e3f7 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -32,6 +32,7 @@ type intro_pattern_expr =
   | IntroOrAndPattern of case_intro_pattern_expr
   | IntroWildcard
   | IntroIdentifier of identifier
+  | IntroAnonymous
 and case_intro_pattern_expr = intro_pattern_expr list list
 
 val pr_intro_pattern : intro_pattern_expr -> Pp.std_ppcmds