Addressing issues with PR#873: performance and use of abbreviation for printing.

We do a couple of changes:

- Splitting notation keys into more categories to make table smaller.
  This should (a priori) make printing faster (see #6416).

- Abbreviations are treated for printing like single notations: they
  are pushed to the scope stack, so that in a situation such as

  Open Scope foo_scope.
  Notation foo := term.
  Open Scope bar_scope.

  one looks for notations first in scope bar_scope, then try to use
  foo, they try for notations in scope foo_scope.

- We seize the opportunity of this commit to simplify
  availability_of_notation which is now integrated to
  uninterp_notation and which does not have to be called explicitly
  anymore.

1 files changed, 13 insertions, 1 deletions

diff --git a/interp/notation.mli b/interp/notation.mli
index 40b7f2c2c9..8cc69f4d1b 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -211,18 +211,27 @@ val declare_uninterpretation : interp_rule -> interpretation -> unit
 val interp_notation : ?loc:Loc.t -> notation -> subscopes ->
       interpretation * (notation_location * scope_name option)
 
-type notation_rule = interp_rule * interpretation * int option
+type notation_rule_core =
+    interp_rule (* kind of notation *)
+  * interpretation (* pattern associated to the notation *)
+  * int option (* number of expected arguments *)
+
+type notation_rule =
+    notation_rule_core
+  * delimiters option (* delimiter to possibly add *)
 
 (** Return the possible notations for a given term *)
 val uninterp_notations : subscopes -> 'a glob_constr_g -> notation_rule list
 val uninterp_cases_pattern_notations : subscopes -> 'a cases_pattern_g -> notation_rule list
 val uninterp_ind_pattern_notations : subscopes -> inductive -> notation_rule list
 
+(*
 (** Test if a notation is available in the scopes 
    context [scopes]; if available, the result is not None; the first 
    argument is itself not None if a delimiters is needed *)
 val availability_of_notation : scope_name option * notation -> subscopes ->
   (scope_name option * delimiters option) option
+ *)
 
 (** {6 Miscellaneous} *)
 
@@ -233,6 +242,9 @@ val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) ->
 val exists_notation_in_scope : scope_name option -> notation ->
       bool -> interpretation -> bool
 
+(** Checks for already existing notations *)
+val exists_notation_interpretation_in_scope : scope_name option -> notation -> bool
+
 (** Declares and looks for scopes associated to arguments of a global ref *)
 val declare_arguments_scope :
   bool (** true=local *) -> GlobRef.t -> scope_name option list -> unit