From d4dac391db9e3be7a45d26e2da9007997b79587d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Mon, 4 Jun 2018 14:28:11 +0200
Subject: Documenting the API change.

---
 dev/doc/changes.md | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'dev/doc')

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 4838dd734..bb8189efc 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -28,6 +28,10 @@ Proof engine
   should indicate what the canonical form is. An important change is
   the move of `Globnames.global_reference` to `Names.GlobRef.t`.
 
+- Unification API returns `evar_map option` instead of `bool * evar_map`
+  with the guarantee that the `evar_map` was unchanged if the boolean
+  was false.
+
 ML Libraries used by Coq
 
 - Introduction of a "Smart" module for collecting "smart*" functions, e.g.
-- 
cgit v1.2.3