Moving bullets (-, +, *) into stand-alone commands instead of being

part of a tactic.
WARNING: Coqide needs to be adapted.


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

2 files changed, 17 insertions, 21 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 756f1d518..02d266336 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -37,7 +37,6 @@ let check_command = Gram.entry_create "vernac:check_command"
 
 let tactic_mode = Gram.entry_create "vernac:tactic_command"
 let noedit_mode = Gram.entry_create "vernac:noedit_command"
-let bullet = Gram.entry_create "vernac:bullet"
 let subprf = Gram.entry_create "vernac:subprf"
 
 let class_rawexpr = Gram.entry_create "vernac:class_rawexpr"
@@ -70,7 +69,7 @@ let default_command_entry =
 
 let no_hook _ _ = ()
 GEXTEND Gram
-  GLOBAL: vernac gallina_ext tactic_mode noedit_mode bullet subprf subgoal_command;
+  GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command;
   vernac: FIRST
     [ [ IDENT "Time"; v = vernac -> VernacTime v
       | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v)
@@ -97,22 +96,20 @@ GEXTEND Gram
       | -> locality_flag := None ] ]
   ;
   noedit_mode:
-    [ [ c = subgoal_command -> c None None] ]
+    [ [ c = subgoal_command -> c None] ]
   ;
   tactic_mode:
   [ [ gln = OPT[n=natural; ":" -> n];
-      tac = subgoal_command -> tac gln None 
-    | b = bullet; tac = subgoal_command -> tac None (Some b)] ]
-  ;
-  bullet:
-  [ [ "-" -> Dash
-    | "*" -> Star
-    | "+" -> Plus ] ]
+      tac = subgoal_command -> tac gln 
+    | tac = subgoal_command -> tac None ] ]
   ;
 
   subprf:
   [ [
-      "{" -> VernacSubproof None
+      "-" -> VernacBullet Dash
+    | "*" -> VernacBullet Star
+    | "+" -> VernacBullet Plus
+    | "{" -> VernacSubproof None
     | "}" -> VernacEndSubproof
     ] ]
   ;
@@ -120,12 +117,12 @@ GEXTEND Gram
 
 
   subgoal_command: 
-    [ [ c = check_command; "." -> fun g _ -> c g
+    [ [ c = check_command; "." -> fun g -> c g
       | tac = Tactic.tactic;
         use_dft_tac = [ "." -> false | "..." -> true ] ->
-          (fun g b ->
+          (fun g ->
             let g = Option.default 1 g in
-            VernacSolve(g,b,tac,use_dft_tac)) ] ]
+            VernacSolve(g,tac,use_dft_tac)) ] ]
   ;
   located_vernac:
     [ [ v = vernac -> loc, v ] ]
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index e10d42b9d..c858439e6 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -754,14 +754,8 @@ let rec pr_vernac = function
       hov 2 (str"Include " ++
 	     prlist_with_sep (fun () -> str " <+ ") pr_m mexprs)
   (* Solving *)
-  | VernacSolve (i,b,tac,deftac) ->
+  | VernacSolve (i,tac,deftac) ->
       (if i = 1 then mt() else int i ++ str ": ") ++
-      begin match b with
-      | None -> mt ()
-      | Some Dash -> str"-"
-      | Some Star -> str"*"
-      | Some Plus -> str"+"
-      end ++
       pr_raw_tactic tac
       ++ (try if deftac then str ".." else mt ()
       with UserError _|Loc.Exc_located _ -> mt())
@@ -979,6 +973,11 @@ let rec pr_vernac = function
       str "Proof using" ++spc()++ prlist pr_lident l ++ spc() ++
       str "with" ++ spc() ++pr_raw_tactic te
   | VernacProofMode s -> str ("Proof Mode "^s)
+  | VernacBullet b -> begin match b with
+      | Dash -> str"-"
+      | Star -> str"*"
+      | Plus -> str"+"
+  end ++ spc()
   | VernacSubproof None -> str "BeginSubproof"
   | VernacSubproof (Some i) -> str "BeginSubproof " ++ pr_int i
   | VernacEndSubproof -> str "EndSubproof"