From b213bae73ca927874275a896482246b2ee761b7b Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Thu, 8 Aug 2013 18:52:17 +0000
Subject: Support Proof General

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16678 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 intf/vernacexpr.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 2f8ab38133..9a26668cd0 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -222,6 +222,7 @@ type 'a stm_vernac =
   | Finish
   | Observe of Stateid.state_id
   | Command of 'a (* An out of flow command not to be recorded by Stm *)
+  | PGLast of 'a (* To ease the life of PG *)
 
 (** {6 Types concerning the module layer} *)
 
-- 
cgit v1.2.3