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.

---
 intf/vernacexpr.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 6a3c1165fe..850f06f87b 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -75,6 +75,7 @@ type printable =
   | PrintAbout of reference or_by_notation
   | PrintImplicit of reference or_by_notation
   | PrintAssumptions of bool * bool * reference or_by_notation
+  | PrintStrategy of reference or_by_notation option
 
 type search_about_item =
   | SearchSubPattern of constr_pattern_expr
-- 
cgit v1.2.3