From 63b530234e0b19323a50c52434a7439518565c81 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 24 May 2018 03:15:17 +0200
Subject: [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.
---
 printing/genprint.mli | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'printing/genprint.mli')

diff --git a/printing/genprint.mli b/printing/genprint.mli
index fd5dd7259e..1a31025a9a 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)
-- 
cgit v1.2.3