From 2d015514b890c2c6f5506fa15c5b592209a590ae Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 19 Mar 2014 19:10:43 +0100
Subject: Adding a Print Strategy vernacular command. It allows to check the
 transparent status of variables and constants.

---
 printing/ppvernac.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 430dfab4d8..ecc80c2cf3 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -459,6 +459,8 @@ let pr_printable = function
   in
   str cmd ++ spc() ++ pr_smart_global qid
 | PrintNamespace dp -> str "Print Namespace" ++ pr_dirpath dp
+| PrintStrategy None -> str "Print Strategies"
+| PrintStrategy (Some qid) -> str "Print Strategy" ++ pr_smart_global qid
 in
 
 let pr_using e = str (Proof_using.to_string e) in
-- 
cgit v1.2.3