diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/user-overlays/06745-ejgallego-located+vernac.sh | 13 | ||||
| -rw-r--r-- | dev/doc/changes.md | 8 |
2 files changed, 21 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh b/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh new file mode 100644 index 0000000000..d1d61fec2e --- /dev/null +++ b/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh @@ -0,0 +1,13 @@ +if [ "$CI_PULL_REQUEST" = "6745" ] || [ "$CI_BRANCH" = "located+vernac" ]; then + ltac2_CI_BRANCH=located+vernac + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + Equations_CI_BRANCH=located+vernac + Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + fiat_parsers_CI_BRANCH=located+vernac + fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat + + Elpi_CI_BRANCH=located+vernac + Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git +fi diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 16a31790a4..ab78b0956f 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -49,6 +49,14 @@ We changed the type of the following functions: a functional way. The old style of passing `evar_map`s as references is not supported anymore. +Changes in the abstract syntax tree: + +- The practical totality of the AST has been nodified using + `CAst.t`. This means that all objects coming from parsing will be + indeed wrapped in a `CAst.t`. `Loc.located` is on its way to + deprecation. Some minor interfaces changes have resulted from + this. + We have changed the representation of the following types: - `Lib.object_prefix` is now a record instead of a nested tuple. |