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).
---
 API/API.mli | 16 +++++-----------
 1 file changed, 5 insertions(+), 11 deletions(-)

(limited to 'API/API.mli')

diff --git a/API/API.mli b/API/API.mli
index 5804a82f64..6a7b2fc9a5 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -3184,6 +3184,10 @@ sig
                        | NCast of notation_constr * notation_constr Misctypes.cast_type
   type interpretation = (Names.Id.t * (subscopes * notation_var_instance_type)) list *
     notation_constr
+  type precedence = int
+  type parenRelation =
+    | L | E | Any | Prec of precedence
+  type tolerability = precedence * parenRelation
 end
 
 module Tactypes :
@@ -4179,16 +4183,6 @@ sig
                                                     'a -> Notation_term.notation_constr -> Glob_term.glob_constr
 end
 
-module Ppextend :
-sig
-
-  type precedence = int
-  type parenRelation =
-    | L | E | Any | Prec of precedence
-  type tolerability = precedence * parenRelation
-
-end
-
 module Notation :
 sig
   type cases_pattern_status = bool
@@ -4880,7 +4874,7 @@ sig
   val pr_with_comments : ?loc:Loc.t -> Pp.t -> Pp.t
   val pr_lident : Names.Id.t Loc.located -> Pp.t
   val pr_lname : Names.Name.t Loc.located -> Pp.t
-  val prec_less : int -> int * Ppextend.parenRelation -> bool
+  val prec_less : int -> int * Notation_term.parenRelation -> bool
   val pr_constr_expr : Constrexpr.constr_expr -> Pp.t
   val pr_lconstr_expr : Constrexpr.constr_expr -> Pp.t
   val pr_constr_pattern_expr : Constrexpr.constr_pattern_expr -> Pp.t
-- 
cgit v1.2.3