aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/ci/user-overlays/08726-herbelin-master+more-stable-meaning-to-Discharge-flag.sh23
-rw-r--r--dev/doc/changes.md4
2 files changed, 27 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/08726-herbelin-master+more-stable-meaning-to-Discharge-flag.sh b/dev/ci/user-overlays/08726-herbelin-master+more-stable-meaning-to-Discharge-flag.sh
new file mode 100644
index 0000000000..242b177d71
--- /dev/null
+++ b/dev/ci/user-overlays/08726-herbelin-master+more-stable-meaning-to-Discharge-flag.sh
@@ -0,0 +1,23 @@
+if [ "$CI_PULL_REQUEST" = "8726" ] || [ "$CI_BRANCH" = "master+more-stable-meaning-to-Discharge-flag" ]; then
+
+ fiat_parsers_CI_BRANCH=master+change-for-coq-pr8726
+ fiat_parsers_CI_REF=master+change-for-coq-pr8726
+ fiat_parsers_CI_GITURL=https://github.com/herbelin/fiat
+
+ elpi_CI_BRANCH=coq-master+fix-global-pr8726
+ elpi_CI_REF=coq-master+fix-global-pr8726
+ elpi_CI_GITURL=https://github.com/herbelin/coq-elpi
+
+ equations_CI_BRANCH=master+fix-global-pr8726
+ equations_CI_REF=master+fix-global-pr8726
+ equations_CI_GITURL=https://github.com/herbelin/Coq-Equations
+
+ mtac2_CI_BRANCH=master+fix-global-pr8726
+ mtac2_CI_REF=master+fix-global-pr8726
+ mtac2_CI_GITURL=https://github.com/herbelin/Mtac2
+
+ paramcoq_CI_BRANCH=master+fix-global-pr8726
+ paramcoq_CI_REF=master+fix-global-pr8726
+ paramcoq_CI_GITURL=https://github.com/herbelin/paramcoq
+
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 339ac2d9b7..cc58222fbf 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -5,6 +5,10 @@
- Functions and types deprecated in 8.10 have been removed in Coq
8.11.
+- Type Decl_kinds.locality has been restructured, see commit
+ message. Main change to do generally is to change the flag "Global"
+ to "Global ImportDefaultBehavior".
+
## Changes between Coq 8.9 and Coq 8.10
### ML4 Pre Processing