diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-18 18:57:34 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-18 18:57:34 +0100 |
| commit | 6af0969228e57c611e5a0876efe613055de342cd (patch) | |
| tree | cfeb33115bb53bc41c588cf75dc70ef515eceff9 /CHANGES | |
| parent | 3690e568a36f8b418ec9c253a3188403f53021ba (diff) | |
| parent | 6734614d8ace6860e3deb1861611ba4b012cfae1 (diff) | |
Merge PR #6380: Add tactics to reset and display the Ltac profile
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 5 |
1 files changed, 3 insertions, 2 deletions
@@ -34,6 +34,7 @@ Tactics - The tactic "romega" is also aware now of the bodies of context variables. - Tactic "decide equality" now able to manage constructors which contain proofs. +- Added tactics reset ltac profile, show ltac profile (and variants) Vernacular Commands @@ -288,7 +289,7 @@ Changes from 8.6 to 8.6.1 - Fix bug 5550: "typeclasses eauto with" does not work with section variables. - Bug 5546, qualify datatype constructors when needed in Show Match - Bug #5535, test for Show with -emacs -- Fix bug #5486, don't reverse ids in tuples +- Fix bug #5486, don't reverse ids in tuples - Fixing #5522 (anomaly with free vars of pat) - Fix bug #5526, don't check for nonlinearity in notation if printing only - Fix bug #5255 @@ -310,7 +311,7 @@ Changes from 8.6 to 8.6.1 - show unused intro pattern warning - [future] Be eager when "chaining" already resolved future values. - Opaque side effects -- Fix #5132: coq_makefile generates incorrect install goal +- Fix #5132: coq_makefile generates incorrect install goal - Run non-tactic comands without resilient_command - Univs: fix bug #5365, generation of u+k <= v constraints - make `emit' tail recursive |