From 5db048b7f9cb5d13e44d87a1007ff042eef25fb5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 24 Jul 2017 21:01:23 +0200
Subject: A new step of restructuration of notations.

This allows to issue a more appropriate message when a notation with a
{ } cannot be defined because of an incompatible level. E.g.:

Notation "{ A } + B" := (sumbool A B) (at level 20).
---
 interp/notation.ml  |  1 -
 interp/notation.mli |  1 -
 interp/ppextend.ml  |  9 +--------
 interp/ppextend.mli | 10 ++--------
 4 files changed, 3 insertions(+), 18 deletions(-)

(limited to 'interp')

diff --git a/interp/notation.ml b/interp/notation.ml
index c7bf0e36bf..c373faf680 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -41,7 +41,6 @@ open Context.Named.Declaration
 (**********************************************************************)
 (* Scope of symbols *)
 
-type level = precedence * tolerability list * notation_var_internalization_type list
 type delimiters = string
 type notation_location = (DirPath.t * DirPath.t) * string
 
diff --git a/interp/notation.mli b/interp/notation.mli
index 5f6bfa35f0..f9f247fe10 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -21,7 +21,6 @@ open Ppextend
 (** A scope is a set of interpreters for symbols + optional
    interpreter and printers for integers + optional delimiters *)
 
-type level = precedence * tolerability list * notation_var_internalization_type list
 type delimiters = string
 type scope
 type scopes (** = [scope_name list] *)
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index 2bbe87bbca..3ebc9b71d2 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -7,17 +7,10 @@
 (************************************************************************)
 
 open Pp
+open Notation_term
 
 (*s Pretty-print. *)
 
-(* Dealing with precedences *)
-
-type precedence = int
-
-type parenRelation = L | E | Any | Prec of precedence
-
-type tolerability = precedence * parenRelation
-
 type ppbox =
   | PpHB of int
   | PpHOVB of int
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index a347a5c7b7..6ff5a42728 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -6,15 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** {6 Pretty-print. } *)
-
-(** Dealing with precedences *)
-
-type precedence = int
+open Notation_term
 
-type parenRelation = L | E | Any | Prec of precedence
-
-type tolerability = precedence * parenRelation
+(** {6 Pretty-print. } *)
 
 type ppbox =
   | PpHB of int
-- 
cgit v1.2.3