[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.

6 files changed, 8 insertions, 8 deletions

diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 702b83034..4e7c8b754 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -251,7 +251,7 @@ END
 let pr_by_arg_tac _prc _prlc prtac opt_c =
   match opt_c with
     | None -> mt ()
-    | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_term.E) t)
+    | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_gram.E) t)
 
 ARGUMENT EXTEND by_arg_tac
   TYPED AS tactic_opt
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index e5a4f090e..ff697e3c7 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -66,7 +66,7 @@ val wit_by_arg_tac :
   Geninterp.Val.t option) Genarg.genarg_type
 
 val pr_by_arg_tac : 
-  (int * Notation_term.parenRelation -> raw_tactic_expr -> Pp.t) ->
+  (int * Notation_gram.parenRelation -> raw_tactic_expr -> Pp.t) ->
   raw_tactic_expr option -> Pp.t
 
 val test_lpar_id_colon : unit Pcoq.Gram.entry
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 3dfe308a5..b29af6680 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -18,7 +18,7 @@ open Genarg
 open Geninterp
 open Stdarg
 open Libnames
-open Notation_term
+open Notation_gram
 open Misctypes
 open Locus
 open Decl_kinds
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 799a52cc8..5d2a99618 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -17,7 +17,7 @@ open Names
 open Misctypes
 open Environ
 open Constrexpr
-open Notation_term
+open Notation_gram
 open Tacexpr
 
 type 'a grammar_tactic_prod_item_expr =
@@ -153,5 +153,5 @@ val pr_value : tolerability -> Val.t -> Pp.t
 
 val ltop : tolerability
 
-val make_constr_printer : (env -> Evd.evar_map -> Notation_term.tolerability -> 'a -> Pp.t) ->
+val make_constr_printer : (env -> Evd.evar_map -> tolerability -> 'a -> Pp.t) ->
   'a Genprint.top_printer
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 138b42e54..fbfbdb110 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -64,7 +64,7 @@ DECLARE PLUGIN "ssreflect_plugin"
  * we thus save the lexer to restore it at the end of the file *)
 let frozen_lexer = CLexer.get_keyword_state () ;;
 
-let tacltop = (5,Notation_term.E)
+let tacltop = (5,Notation_gram.E)
 
 let pr_ssrtacarg _ _ prt = prt tacltop
 ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY pr_ssrtacarg
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index 2ac7c7e26..7cd3751ce 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -14,11 +14,11 @@ open Ltac_plugin
 
 val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
 val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
-val pr_ssrtacarg : 'a -> 'b -> (Notation_term.tolerability -> 'c) -> 'c
+val pr_ssrtacarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c) -> 'c
 
 val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
 val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
-val pr_ssrtclarg : 'a -> 'b -> (Notation_term.tolerability -> 'c -> 'd) -> 'c -> 'd
+val pr_ssrtclarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c -> 'd) -> 'c -> 'd
 
 val add_genarg : string -> ('a -> Pp.t) -> 'a Genarg.uniform_genarg_type