Break circular dependency Proof_global -> Vernacexpr -> Proof_global.

Fixes bug #2547 ( http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2547 )

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

5 files changed, 14 insertions, 15 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3593239023..6dae6ee233 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -103,9 +103,9 @@ GEXTEND Gram
     | b = bullet; tac = subgoal_command -> tac None (Some b)] ]
   ;
   bullet:
-  [ [ "-" -> Proof_global.Bullet.Dash
-    | "*" -> Proof_global.Bullet.Star
-    | "+" -> Proof_global.Bullet.Plus ] ]
+  [ [ "-" -> Dash
+    | "*" -> Star
+    | "+" -> Plus ] ]
   ;
   subgoal_command: 
     [ [ c = check_command; "." -> fun g _ -> c g
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index ebd8175d74..db6f0e6216 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -747,9 +747,9 @@ let rec pr_vernac = function
       (if i = 1 then mt() else int i ++ str ": ") ++
       begin match b with
       | None -> mt ()
-      | Some Proof_global.Bullet.Dash -> str"-"
-      | Some Proof_global.Bullet.Star -> str"*"
-      | Some Proof_global.Bullet.Plus -> str"+"
+      | Some Dash -> str"-"
+      | Some Star -> str"*"
+      | Some Plus -> str"+"
       end ++
       pr_raw_tactic tac
       ++ (try if deftac then str ".." else mt ()
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 780f2eeda6..186472be27 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -315,10 +315,7 @@ module Bullet = struct
   open Store.Field
 
 
-  type t = 
-    | Dash
-    | Star
-    | Plus
+  type t = Vernacexpr.bullet
 
   type behavior = {
     name : string;
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index f9dbe3438a..2f9f4a549d 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -102,10 +102,7 @@ val maximal_unfocus : 'a Proof.focus_kind -> Proof.proof -> unit
 (**********************************************************)
 
 module Bullet : sig
-  type t = 
-    | Dash
-    | Star
-    | Plus
+  type t = Vernacexpr.bullet
 
   (** A [behavior] is the data of a put function which
       is called when a bullet prefixes a tactic, together
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index de121e93db..6ea4e263ff 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -195,6 +195,11 @@ type scheme =
 
 type inline = int option (* inlining level, none for no inlining *)
 
+type bullet =
+    | Dash
+    | Star
+    | Plus
+
 type vernac_expr =
   (* Control *)
   | VernacList of located_vernac_expr list
@@ -271,7 +276,7 @@ type vernac_expr =
 
   (* Solving *)
 
-  | VernacSolve of int * Proof_global.Bullet.t option * raw_tactic_expr * bool
+  | VernacSolve of int * bullet option * raw_tactic_expr * bool
   | VernacSolveExistential of int * constr_expr
 
   (* Auxiliary file and library management *)