From 6eb42e53ffafd9aed3c12805c6a228acccc03827 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 8 Apr 2017 20:08:01 +0200
Subject: [location] Document changes.

---
 dev/doc/changes.txt | 8 ++++++++
 lib/loc.mli         | 5 ++++-
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 7f915b7819..10c3f396e4 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -51,6 +51,14 @@ In Constrexpr_ops:
   interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second
   ones were preserving the original sharing of the type.
 
+Location handling has been reworked, Loc.ghost has been removed in
+favor of an option type. All objects carrying a source code location
+have been switched to `'a Loc.located == Loc.t option * a'`, which
+should be treated as private (that is, ok to match against, but
+forbidden to manually build), and is mandatory to use for objects with
+location. This policy has been implemented in the whole code base,
+including all the ASTs for vernacular, gallina, and tactics.
+
 ** Ltac API **
 
 Many Ltac specific API has been moved in its own ltac/ folder. Amongst other
diff --git a/lib/loc.mli b/lib/loc.mli
index 110920d5ad..ec79ced5d3 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -51,8 +51,11 @@ val raise : ?loc:t -> exn -> 'a
 type 'a located = t option * 'a
 (** Embed a location in a type *)
 
-(** Warning, this API is experimental  *)
+(* We would like in the future:
+ * type 'a located = private { tag: t option; obj: 'a; }
+ *)
 
+(** Warning, this API is experimental  *)
 val to_pair : 'a located -> t option * 'a
 val tag : ?loc:t -> 'a -> 'a located
 val obj : 'a located -> 'a
-- 
cgit v1.2.3