Ajout FreshId

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

6 files changed, 10 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 2e66d182c..65fb63776 100644
--- a/CHANGES
+++ b/CHANGES
@@ -45,6 +45,8 @@ Implicit arguments
   implicits (like constants and variables)
 - Set Implicit Arguments is strict by default in new syntax
 - Implicit Arguments flags are now synchronous with reset
+- New switch "Unset/Set Printing Implicits" to globally control
+  printing of implicits
 
 Grammar extensions
 
@@ -64,6 +66,7 @@ Library
 Tactic language
 
 - Fail tactic now accepts a failure message
+- New primitive tactic "FreshId" to generate new names
 
 Tactics
 
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 57f47ca15..b3fd4fa19 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -208,6 +208,7 @@ GEXTEND Gram
 	  ConstrMayEval (ConstrContext (id,c))
       | IDENT "Check"; c = Constr.constr ->
 	  ConstrMayEval (ConstrTypeOf c)
+      | IDENT "FreshId"; s = OPT STRING -> TacFreshId s
       | r = reference -> Reference r
       | ta = tactic_arg0 -> ta ] ]
   ;
@@ -218,6 +219,7 @@ GEXTEND Gram
 	  ConstrMayEval (ConstrContext (id,c))
       | IDENT "Check"; c = Constr.constr ->
 	  ConstrMayEval (ConstrTypeOf c)
+      | IDENT "FreshId"; s = OPT STRING -> TacFreshId s
       | r = reference; la = LIST1 tactic_arg0 -> TacCall (loc,r,la)
       | r = reference -> Reference r
       | ta = tactic_arg0 -> ta ] ]
diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4
index 200076557..712eefe92 100644
--- a/parsing/g_ltacnew.ml4
+++ b/parsing/g_ltacnew.ml4
@@ -119,6 +119,8 @@ GEXTEND Gram
 	  TacArg(ConstrMayEval (ConstrContext (id,c)))
       | IDENT "check"; c = Constr.lconstr ->
 	  TacArg(ConstrMayEval (ConstrTypeOf c))
+      | IDENT "freshid"; s = OPT STRING ->
+	  TacFreshId s
       | "'"; c = Constr.constr -> TacArg(ConstrMayEval(ConstrTerm c))
       | r = reference; la = LIST1 tactic_arg ->
           TacArg(TacCall (loc,r,la))
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 3022fcbb1..9c23d0ba5 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -647,6 +647,7 @@ and pr_tacarg0 = function
   | ConstrMayEval (ConstrTerm c) -> str "'" ++ pr_constr c
   | ConstrMayEval c -> pr_may_eval pr_constr pr_cst c
   | Integer n -> int n
+  | TacFreshId sopt -> str "FreshId" ++ pr_opt qstring sopt
   | (TacCall _ | Tacexp _) as t -> str "(" ++ pr_tacarg1 t ++ str ")"
 
 and pr_tacarg1 = function
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 860a91aff..f0bace786 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -201,6 +201,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg =
   | Integer        of int
   | TacCall        of loc *
       'ref * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg list
+  | TacFreshId     of string option
   | Tacexp of 'tac
 
 type raw_tactic_expr =
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 0c4f571d7..30433b491 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -481,6 +481,7 @@ and pr_tacarg env = function
   | TacVoid -> str "()"
   | Reference r -> pr_ref r
   | ConstrMayEval (ConstrTerm c) -> pr_constr env c
+  | TacFreshId sopt -> str "FreshId" ++ pr_opt qstring sopt
   | (ConstrMayEval _|TacCall _|Tacexp _|Integer _) as a ->
       str "'" ++ pr_tac env (latom,E) (TacArg a)