From 85d5b246b0fbf845c6c61ffac6f0e2563c237d69 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 26 Jul 2018 09:54:42 -0400 Subject: Update CHANGES --- CHANGES | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index a42c44c09b..b1f9d46ed8 100644 --- a/CHANGES +++ b/CHANGES @@ -65,6 +65,15 @@ Standard Library - Added `Ndigits.N2Bv_sized`, and proved some lemmas about it. +- The scopes `int_scope` and `uint_scope` have been renamed to + `dec_int_scope` and `dec_uint_scope`, to clash less with ssreflect + and other packages. They are still delimited by `%int` and `%uint`. + +- Numeral syntax for `nat` is no longer available without loading the + entire prelude (`Require Import Coq.Init.Prelude`). This only + impacts users running Coq without the init library (`-nois` or + `-noinit`) and also issuing `Require Import Coq.Init.Datatypes`. + Tools - Coq_makefile lets one override or extend the following variables from @@ -98,6 +107,8 @@ Vernacular Commands overwritting the opacity set of the hint database. - Added generic syntax for “attributes”, as in: `#[local] Lemma foo : bar.` +- Added the `Numeral Notation` command for registering decimal numeral + notations for custom types - The `Set SsrHave NoTCResolution` command no longer has special global scope. If you want the previous behavior, use `Global Set SsrHave NoTCResolution`. -- cgit v1.2.3 From 6dcbbeb95682bbf470e58e25e0a357a84c3283b6 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 23 Aug 2018 11:03:29 -0400 Subject: Make Numeral Notation follow Import, not Require Because that's the sane thing to do. This will inevitably cause issues for projects which do not `Import Coq.Strings.Ascii` before trying to use ascii notations. We also move the syntax plugin for `int31` notations from `Cyclic31` to `Int31`, so that users (like CompCert) who merely `Require Import Coq.Numbers.Cyclic.Int31.Int31` get the `int31` numeral syntax. Since `Cyclic31` `Export`s `Int31`, this should not cause any additional incompatibilities. --- CHANGES | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index b1f9d46ed8..5d1c9a9c2d 100644 --- a/CHANGES +++ b/CHANGES @@ -69,6 +69,24 @@ Standard Library `dec_int_scope` and `dec_uint_scope`, to clash less with ssreflect and other packages. They are still delimited by `%int` and `%uint`. +- Syntax notations for `string`, `ascii`, `Z`, `positive`, `N`, `R`, + and `int31` are no longer available merely by `Require`ing the files + that define the inductives. You must `Import` `Coq.Strings.String`, + `Coq.Strings.Ascii`, `Coq.ZArith.BinIntDef`, `Coq.PArith.BinPosDef`, + `Coq.NArith.BinNatDef`, `Coq.Reals.Rdefinitions`, and + `Coq.Numbers.Cyclic.Int31.Int31`, respectively, to be able to use + these notations. Note that passing `-compat 8.8` or issuing + `Require Import Coq.Compat.Coq88` will make these notations + available. Users wishing to port their developments automatically + may download `fix.py` from + + and run a command like `while true; do make -Okj 2>&1 | + /path/to/fix.py; done` and get a cup of coffee. (This command must + be manually interrupted once the build finishes all the way though. + Note also that this method is not fail-proof; you may have to adjust + some scopes if you were relying on string notations not being + available even when `string_scope` was open.) + - Numeral syntax for `nat` is no longer available without loading the entire prelude (`Require Import Coq.Init.Prelude`). This only impacts users running Coq without the init library (`-nois` or -- cgit v1.2.3