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.

1 files changed, 17 insertions, 15 deletions

diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 280ccfd21..576c5b943 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -10,24 +10,28 @@ open Names
 open Notation_term
 open Glob_term
 
-(** Utilities about [notation_constr] *)
+(** {5 Utilities about [notation_constr]} *)
 
-(** Translate a [glob_constr] into a notation given the list of variables
-    bound by the notation; also interpret recursive patterns           *)
+val eq_notation_constr : notation_constr -> notation_constr -> bool
 
-val notation_constr_of_glob_constr : notation_interp_env ->
-  glob_constr -> notation_constr
+(** Substitution of kernel names in interpretation data                *)
 
+val subst_interpretation :
+  Mod_subst.substitution -> interpretation -> interpretation
+                                                
 (** Name of the special identifier used to encode recursive notations  *)
+
 val ldots_var : Id.t
 
-(** Equality of [glob_constr] (warning: only partially implemented) *)
-(** FIXME: nothing to do here *)
-val eq_glob_constr : glob_constr -> glob_constr -> bool
+(** {5 Translation back and forth between [glob_constr] and [notation_constr] *)
 
-val eq_notation_constr : notation_constr -> notation_constr -> bool
+(** Translate a [glob_constr] into a notation given the list of variables
+    bound by the notation; also interpret recursive patterns           *)
+
+val notation_constr_of_glob_constr : notation_interp_env ->
+  glob_constr -> notation_constr
 
-(** Re-interpret a notation as a [glob_constr], taking care of binders     *)
+(** Re-interpret a notation as a [glob_constr], taking care of binders *)
 
 val glob_constr_of_notation_constr_with_binders : Loc.t ->
   ('a -> Name.t -> 'a * Name.t) ->
@@ -36,6 +40,8 @@ val glob_constr_of_notation_constr_with_binders : Loc.t ->
 
 val glob_constr_of_notation_constr : Loc.t -> notation_constr -> glob_constr
 
+(** {5 Matching a notation pattern against a [glob_constr] *)
+
 (** [match_notation_constr] matches a [glob_constr] against a notation
     interpretation; raise [No_match] if the matching fails   *)
 
@@ -55,9 +61,5 @@ val match_notation_constr_ind_pattern :
   ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) *
     (int * cases_pattern list)
 
-(** Substitution of kernel names in interpretation data                *)
-
-val subst_interpretation :
-  Mod_subst.substitution -> interpretation -> interpretation
+(** {5 Matching a notation pattern against a [glob_constr] *)
 
-val add_patterns_for_params : inductive -> cases_pattern list -> cases_pattern list