From 5b9981239c3192d20d7db2de1248a63b59cbf44a Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Tue, 17 May 2011 10:31:45 +0000
Subject: 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
---
 proofs/proof_global.ml  | 5 +----
 proofs/proof_global.mli | 5 +----
 2 files changed, 2 insertions(+), 8 deletions(-)

(limited to 'proofs')

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
-- 
cgit v1.2.3