Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et fail peuvent maintenant être des listes de string, int et variables ltac

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

2 files changed, 22 insertions, 15 deletions

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 313886e9ae..1deffe6d35 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -45,7 +45,7 @@ GEXTEND Gram
       [ ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0, ta1)
       | ta = tactic_expr; ";"; 
 	"["; lta = LIST0 OPT tactic_expr SEP "|"; "]" ->
-	  let lta = List.map (function None -> TacId "" | Some t -> t) lta in 
+	  let lta = List.map (function None -> TacId [] | Some t -> t) lta in 
 	  TacThens (ta, lta) ]
     | "4"
       [ ]
@@ -80,9 +80,10 @@ GEXTEND Gram
 	  TacFirst l
       | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
 	  TacSolve l
-      | IDENT "idtac"; s = [ s = STRING -> s | -> ""] -> TacId s		
+      | IDENT "complete" ; ta = tactic_expr -> TacComplete ta
+      | IDENT "idtac"; l = LIST0 message_token -> TacId l
       | IDENT "fail"; n = [ n = int_or_var -> n | -> fail_default_value ];
-	  s = [ s = STRING -> s | -> ""] -> TacFail (n,s)
+	  l = LIST0 message_token -> TacFail (n,l)
       | IDENT "external"; com = STRING; req = STRING; la = LIST1 tactic_arg ->
 	  TacArg (TacExternal (loc,com,req,la))
       | st = simple_tactic -> TacAtom (loc,st)
@@ -172,14 +173,13 @@ GEXTEND Gram
     [ [ mrl = LIST1 match_rule SEP "|" -> mrl
       | "|"; mrl = LIST1 match_rule SEP "|" -> mrl ] ]
   ;
+  message_token:
+    [ [ id = identref -> MsgIdent (AI id)
+      | s = STRING -> MsgString s
+      | n = integer -> MsgInt n ] ]
+  ;
 
   (* Definitions for tactics *)
-(*
-  deftok:
-    [ [ IDENT "Meta"
-      | IDENT "Tactic" ] ]
-  ;
-*)
   tacdef_body:
     [ [ name = identref; it=LIST1 input_fun; ":="; body = tactic_expr ->
 	  (name, TacFun (it, body))
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index ea693afa43..d9ef227f69 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -122,6 +122,11 @@ let pr_with_names = function
   | None -> mt ()
   | Some ipat -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat)
 
+let rec pr_message_token prid = function
+  | MsgString s -> qs s
+  | MsgInt n -> int n
+  | MsgIdent id -> prid id
+
 let rec pr_raw_generic prc prlc prtac prref x =
   match Genarg.genarg_tag x with
   | BoolArgType -> pr_arg str (if out_gen rawwit_bool x then "true" else "false")
@@ -373,7 +378,7 @@ let pr_assumption prlc prc ipat c = match ipat with
       spc() ++ prc c ++ pr_with_names ipat
 
 let pr_by_tactic prt = function
-  | TacId "" -> mt ()
+  | TacId [] -> mt ()
   | tac -> spc() ++ str "by " ++ prt tac
 
 let pr_occs pp = function
@@ -510,6 +515,7 @@ let ltactical = 3
 let lorelse = 2
 let llet = 1
 let lfun = 1
+let lcomplete = 1
 let labstract = 3
 let lmatch = 1
 let latom = 0
@@ -845,16 +851,17 @@ let rec pr_tac env inherited tac =
       hov 1 (pr_tac env (lorelse,L) t1 ++ str " ||" ++ brk (1,1) ++
              pr_tac env (lorelse,E) t2),
       lorelse
-  | TacFail (ArgArg 0,"") -> str "fail", latom
-  | TacFail (n,s) -> 
+  | TacFail (n,l) -> 
       str "fail" ++ (if n=ArgArg 0 then mt () else pr_arg (pr_or_var int) n) ++
-      (if s="" then mt() else (spc() ++ qs s)), latom
+      prlist (pr_arg (pr_message_token pr_ident)) l, latom
   | TacFirst tl ->
       str "first" ++ spc () ++ pr_seq_body (pr_tac env ltop) tl, llet
   | TacSolve tl ->
       str "solve" ++ spc () ++ pr_seq_body (pr_tac env ltop) tl, llet
-  | TacId "" -> str "idtac", latom
-  | TacId s -> str "idtac" ++ (qs s), latom
+  | TacComplete t ->
+      str "complete" ++ spc () ++ pr_tac env (lcomplete,E) t, lcomplete
+  | TacId l ->
+      str "idtac" ++ prlist (pr_arg (pr_message_token pr_ident)) l, latom
   | TacAtom (loc,TacAlias (_,s,l,_)) ->
       pr_with_comments loc
         (pr_extend env (level_of inherited) s (List.map snd l)),