From b6b98a67c65d7aeeeeca12d1ccb9d55b654c554d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 2 Jun 2016 15:12:05 +0200
Subject: A slight phase of documentation and uniformization of names of
 functions about interpretation, internalization, externalization of
 notations.

Main syntactic changes:
- subst_aconstr_in_glob_constr -> instantiate_notation_constr
  (because aconstr has been renamed to notation_constr long time ago)
- extern_symbol -> extern_notation
  (because symbol.ml has been renamed to notation.ml long time ago)
- documentation of notations_ops.mli

Main semantic changes:
- Notation_ops.eq_glob_constr which was partial eq disappears: use
  glob_constr_eq instead
- In particular, this impacts a change on funind which now use the
  (fully implemented) glob_constr_eq

Somehow, instantiate_notation_constr should be in notation_ops.ml for
symmetry with match_notation_constr but it is bit painful to do.
---
 dev/doc/changes.txt | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'dev')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 53497ff0e5..4a0130bef0 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -2,6 +2,10 @@
 = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
 =========================================
 
+** Notation_ops **
+
+Use Glob_ops.glob_constr_eq instead of Notation_ops.eq_glob_constr.
+
 ** Logging and Pretty Printing: **
 
 * Printing functions have been removed from `Pp.mli`, which is now a
-- 
cgit v1.2.3