[ast] Improve precision of Ast location recognition in serialization.

We follow the suggestions in #402 and turn uses of `Loc.located` in
`vernac` into `CAst.t`. The impact should be low as this change mostly
affects top-level vernaculars.

With this change, we are even closer to automatically map a text
document to its AST in a programmatic way.

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 000000000..d1d61fec2
--- /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 16a31790a..ab78b0956 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.