From e23f495c25749478c0a64c479d888e3671157c7d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 14 Jul 2017 13:27:56 +0200
Subject: Document the changes in API brought by this series of patches.

---
 dev/doc/changes.txt | 20 ++++++++++++++++++++
 library/global.mli  |  7 +++++++
 2 files changed, 27 insertions(+)

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 159be9a582..62c3bc40c1 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -1,3 +1,23 @@
+=========================================
+= CHANGES BETWEEN COQ V8.6 AND COQ V8.8 =
+=========================================
+
+* ML API *
+
+We removed the following functions:
+
+- Universes.unsafe_constr_of_global: use Global.constr_of_global_in_context
+  instead. The returned term contains De Bruijn universe variables. If you don't
+  depend on universes being instantiated, simply drop the context.
+- Universes.unsafe_type_of_global: same as above with
+  Global.type_of_global_in_context
+
+We changed the type of the following functions:
+
+- Global.body_of_constant_body: now also returns the abstract universe context.
+  The returned term contains De Bruijn universe variables.
+- Global.body_of_constant: same as above.
+
 =========================================
 = CHANGES BETWEEN COQ V8.6 AND COQ V8.7 =
 =========================================
diff --git a/library/global.mli b/library/global.mli
index 431747c524..48bcfa989f 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -89,8 +89,15 @@ val constant_of_delta_kn : kernel_name -> constant
 val mind_of_delta_kn : kernel_name -> mutual_inductive
 
 val opaque_tables : unit -> Opaqueproof.opaquetab
+
 val body_of_constant : constant -> (Term.constr * Univ.AUContext.t) option
+(** Returns the body of the constant if it has any, and the polymorphic context
+    it lives in. For monomorphic constant, the latter is empty, and for
+    polymorphic constants, the term contains De Bruijn universe variables that
+    need to be instantiated. *)
+
 val body_of_constant_body : Declarations.constant_body -> (Term.constr * Univ.AUContext.t) option
+(** Same as {!body_of_constant} but on {!Declarations.constant_body}. *)
 
 (** Global universe name <-> level mapping *)
 type universe_names = 
-- 
cgit v1.2.3