From 8d02317cc02ae5d007f5d2486d26bb37865ca0a9 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Thu, 30 Mar 2017 16:28:21 +0200
Subject: hints: add Hint Variables/Constants Opaque/Transparent commands

This gives user control on the transparent state of a hint db. Can
override defaults more easily (report by J. H. Jourdan).

For "core", declare that variables can be unfolded, but no constants
(ensures compatibility with previous auto which allowed conv on closed
terms)

Document Hint Variables
---
 vernac/ppvernac.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'vernac/ppvernac.ml')

diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 56dfaa54a..5fbe1f4e4 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -210,7 +210,10 @@ open Pputils
         | HintsTransparency (l, b) ->
           keyword (if b then "Transparent" else "Opaque")
           ++ spc ()
-          ++ prlist_with_sep sep pr_qualid l
+          ++ (match l with
+              | HintsVariables -> keyword "Variables"
+              | HintsConstants -> keyword "Constants"
+              | HintsReferences l -> prlist_with_sep sep pr_qualid l)
         | HintsMode (m, l) ->
           keyword "Mode"
           ++ spc ()
-- 
cgit v1.2.3