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.
---
 plugins/funind/glob_term_to_relation.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 72205e2bbc..c424fe1226 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1217,7 +1217,7 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool)
 	   if Array.for_all
 	     (fun l ->
 		let (n',nt',is_defined') = List.nth l i in
-		Name.equal n n' && Notation_ops.eq_glob_constr nt nt' && (is_defined : bool) == is_defined')
+		Name.equal n n' && glob_constr_eq nt nt' && (is_defined : bool) == is_defined')
 	     rels_params
 	   then
 	     l := param::!l
-- 
cgit v1.2.3