diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2017-03-30 16:28:21 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2018-07-02 16:27:18 +0200 |
| commit | 8d02317cc02ae5d007f5d2486d26bb37865ca0a9 (patch) | |
| tree | fb2951e3aee66c93f66c2bced46759a99baf3f46 /doc | |
| parent | 02fe76c0c1c3f01c6fb4310dd4450b35f43005da (diff) | |
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
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index d0a0d568e..45667b099 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3422,18 +3422,24 @@ The general command to add a hint to some databases :n:`{+ @ident}` is Adds each :n:`Hint Unfold @ident`. - .. cmdv:: Hint %( Transparent %| Opaque %) @qualid - :name: Hint ( Transparent | Opaque ) + .. cmdv:: Hint Transparent {+ @qualid} + Hint Opaque {+ @qualid} + :name: Hint Transparent; Hint Opaque - This adds a transparency hint to the database, making :n:`@qualid` a - transparent or opaque constant during resolution. This information is used + This adds transparency hints to the database, making :n:`@qualid` + transparent or opaque constants during resolution. This information is used during unification of the goal with any lemma in the database and inside the discrimination network to relax or constrain it in the case of discriminated databases. - .. cmdv:: Hint %( Transparent %| Opaque %) {+ @ident} + .. cmdv:: Hint Variables %( Transparent %| Opaque %) + Hint Constants %( Transparent %| Opaque %) + :name: Hint Variables; Hint Constants - Declares each :n:`@ident` as a transparent or opaque constant. + This sets the transparency flag used during unification of + hints in the database for all constants or all variables, + overwritting the existing settings of opacity. It is advised + to use this just after a :cmd:`Create HintDb` command. .. cmdv:: Hint Extern @num {? @pattern} => @tactic :name: Hint Extern |