diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-07-20 10:56:08 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-07-20 10:56:08 +0200 |
| commit | 2de309b65b379a3c496752aa25f1cfc177644222 (patch) | |
| tree | 2808a0a0a7ce02805488c3d936567ea30d90eaa0 /CHANGES | |
| parent | 161910e3cd7726751ca545262ef8f9c7a69b2a3c (diff) | |
| parent | d308a3ad11f38ce3d504a3d29f9894affdd1fbcc (diff) | |
Merge PR #8089: Remove declare_object for SsrHave NoTCResolution.
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 3 |
1 files changed, 3 insertions, 0 deletions
@@ -75,6 +75,9 @@ Vernacular Commands overwritting the opacity set of the hint database. - Added generic syntax for “attributes”, as in: `#[local] Lemma foo : bar.` +- The `Set SsrHave NoTCResolution` command no longer has special global + scope. If you want the previous behavior, use `Global Set SsrHave + NoTCResolution`. Coq binaries and process model |