aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/ppvernac.ml
diff options
context:
space:
mode:
authorGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-08-08 18:52:17 +0000
committerGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-08-08 18:52:17 +0000
commitb213bae73ca927874275a896482246b2ee761b7b (patch)
tree5320ce95e65b3474ba7a43a43ba1d49c21216310 /printing/ppvernac.ml
parenta936e9ae133f103ed9f781a7aa363c0006a2f178 (diff)
Support Proof General
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16678 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'printing/ppvernac.ml')
-rw-r--r--printing/ppvernac.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index eae6d09d6..b5277b62e 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -482,6 +482,7 @@ let rec pr_vernac = function
| VernacStm (Observe id) ->
str"Stm Observe " ++ str(Stateid.string_of_state_id id)
| VernacStm (Command v) -> str"Stm Command " ++ pr_vernac v
+ | VernacStm (PGLast v) -> str"Stm PGLast " ++ pr_vernac v
(* Proof management *)
| VernacAbortAll -> str "Abort All"