From 398fe8ee23759a1c28d91204aa013beae1dc602b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 12 Oct 2018 18:25:18 +0200 Subject: Cleaning the status of Local Definition and similar. Formerly, knowing if a declaration was to be discharged, to be global but invisible at import, or to be global but visible at import was obtained by combining the parser-level information (i.e. use of Variable/Hypothesis/Let vs use of Axiom/Parameter/Definition/..., use of Local vs Global) with the result of testing whether there were open sections. We change the meaning of the Discharge flag: it does not tell anymore that it was syntactically a Variable/Hypothesis/Let, but tells the expected semantics of the declaration (issuing a warning in the parser-to-interpreter step if the semantics is not the one suggested by the syntax). In particular, the interpretation/command engine becomes independent of the parser. The new "semantic" type is: type import_status = ImportDefaultBehavior | ImportNeedQualified type locality = Discharge | Global of import_status In the process, we found a couple of inconsistencies in the treatment of the locality status. See bug #8722 and test file LocalDefinition.v. --- dev/doc/changes.md | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'dev') 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 -- cgit v1.2.3 From b93a0abded40bec15c6d4105b2d9b418a18ede6c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 12 Oct 2018 22:38:02 +0200 Subject: Overlays for Elpi + Equations + Mtac2 + fiat parsers + paramcoq. --- ...master+more-stable-meaning-to-Discharge-flag.sh | 23 ++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 dev/ci/user-overlays/08726-herbelin-master+more-stable-meaning-to-Discharge-flag.sh (limited to 'dev') 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 -- cgit v1.2.3