diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-31 15:49:09 +0100 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2015-11-02 15:46:40 +0100 |
| commit | 4e643d134f02cfa9a73754c3cf48048541324834 (patch) | |
| tree | 54a8d34fb69fd23b1d5034f13c2cafb20fcc3e0f /CHANGES | |
| parent | 69be6a29cf9f774cb4afe94d76b157ba50984c1d (diff) | |
Adding syntax "Show id" to show goal named id (shelved or not).
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -8,6 +8,7 @@ Vernacular commands - New option "Strict Universe Declaration", set by default. It enforces the declaration of all polymorphic universes appearing in a definition when introducing it. +- New command "Show id" to show goal named id. Tactics @@ -36,7 +37,6 @@ Tactics - Hints costs are now correctly taken into account (potential source of incompatibilities). - API - Some functions from pretyping/typing.ml and their derivatives were potential |