[notations] Split interpretation and parsing of notations

Previously to this patch, `Notation_term` contained information about
both parsing and notation interpretation.

We split notation grammar to a file `parsing/notation_gram` as to make
`interp/` not to depend on some parsing structures such as entries.

5 files changed, 13 insertions, 15 deletions

diff --git a/printing/genprint.ml b/printing/genprint.ml
index 1bb7838a4..fa53a8794 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.ml
@@ -19,15 +19,15 @@ open Geninterp
 (* Printing generic values *)
 
 type 'a with_level =
-  { default_already_surrounded : Notation_term.tolerability;
-    default_ensure_surrounded : Notation_term.tolerability;
+  { default_already_surrounded : Notation_gram.tolerability;
+    default_ensure_surrounded : Notation_gram.tolerability;
     printer : 'a }
 
 type printer_result =
 | PrinterBasic of (unit -> Pp.t)
-| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level
+| PrinterNeedsLevel of (Notation_gram.tolerability -> Pp.t) with_level
 
-type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t
+type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t
 
 type top_printer_result =
 | TopPrinterBasic of (unit -> Pp.t)
diff --git a/printing/genprint.mli b/printing/genprint.mli
index fd5dd7259..1a31025a9 100644
--- a/printing/genprint.mli
+++ b/printing/genprint.mli
@@ -13,15 +13,15 @@
 open Genarg
 
 type 'a with_level =
-  { default_already_surrounded : Notation_term.tolerability;
-    default_ensure_surrounded : Notation_term.tolerability;
+  { default_already_surrounded : Notation_gram.tolerability;
+    default_ensure_surrounded : Notation_gram.tolerability;
     printer : 'a }
 
 type printer_result =
 | PrinterBasic of (unit -> Pp.t)
-| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level
+| PrinterNeedsLevel of (Notation_gram.tolerability -> Pp.t) with_level
 
-type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t
+type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t
 
 type top_printer_result =
 | TopPrinterBasic of (unit -> Pp.t)
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 2a5f38697..e877b3c63 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -19,7 +19,7 @@ open Constr
 open Libnames
 open Pputils
 open Ppextend
-open Notation_term
+open Notation_gram
 open Constrexpr
 open Constrexpr_ops
 open Decl_kinds
@@ -88,8 +88,6 @@ let tag_var = tag Tag.variable
     | Numeral (_,b) -> if b then lposint else lnegint
     | String _ -> latom
 
-  open Notation
-
   let print_hunks n pr pr_patt pr_binders (terms, termlists, binders, binderlists) unps =
     let env = ref terms and envlist = ref termlists and bl = ref binders and bll = ref binderlists in
     let pop r = let a = List.hd !r in r := List.tl !r; a in
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 127c4471c..05f48ec79 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -16,7 +16,7 @@ open Libnames
 open Constrexpr
 open Names
 open Misctypes
-open Notation_term
+open Notation_gram
 
 val prec_less : precedence -> tolerability -> bool
 
diff --git a/printing/printer.mli b/printing/printer.mli
index ac0e12979..7a8b963d2 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -36,7 +36,7 @@ val pr_constr              : constr -> Pp.t
 [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t
 
-val pr_constr_n_env        : env -> evar_map -> Notation_term.tolerability -> constr -> Pp.t
+val pr_constr_n_env        : env -> evar_map -> Notation_gram.tolerability -> constr -> Pp.t
 
 (** Same, but resilient to [Nametab] errors. Prints fully-qualified
     names when [shortest_qualid_of_global] has failed. Prints "??"
@@ -57,7 +57,7 @@ val pr_leconstr_env     : env -> evar_map -> EConstr.t -> Pp.t
 val pr_leconstr         : EConstr.t -> Pp.t
 [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
-val pr_econstr_n_env    : env -> evar_map -> Notation_term.tolerability -> EConstr.t -> Pp.t
+val pr_econstr_n_env    : env -> evar_map -> Notation_gram.tolerability -> EConstr.t -> Pp.t
 
 val pr_etype_env           : env -> evar_map -> EConstr.types -> Pp.t
 val pr_letype_env           : env -> evar_map -> EConstr.types -> Pp.t
@@ -87,7 +87,7 @@ val pr_type_env            : env -> evar_map -> types -> Pp.t
 val pr_type                : types -> Pp.t
 [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
-val pr_closed_glob_n_env   : env -> evar_map -> Notation_term.tolerability -> closed_glob_constr -> Pp.t
+val pr_closed_glob_n_env   : env -> evar_map -> Notation_gram.tolerability -> closed_glob_constr -> Pp.t
 val pr_closed_glob_env     : env -> evar_map -> closed_glob_constr -> Pp.t
 val pr_closed_glob         : closed_glob_constr -> Pp.t
 [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]