From 8d02317cc02ae5d007f5d2486d26bb37865ca0a9 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau 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 --- theories/Init/Logic.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'theories') diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 10ca9ecc9..817581cb2 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -29,6 +29,13 @@ Definition not (A:Prop) := A -> False. Notation "~ x" := (not x) : type_scope. +(** Create the "core" hint database, and set its transparent state for + variables and constants explicitely. *) + +Create HintDb core. +Hint Variables Opaque : core. +Hint Constants Opaque : core. + Hint Unfold not: core. (** [and A B], written [A /\ B], is the conjunction of [A] and [B] -- cgit v1.2.3