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).
---
 printing/ppconstr.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'printing/ppconstr.mli')

diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 8335034851..7546c748d8 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -15,6 +15,7 @@ open Libnames
 open Constrexpr
 open Names
 open Misctypes
+open Notation_term
 
 val extract_lam_binders :
   constr_expr -> local_binder_expr list * constr_expr
@@ -24,7 +25,7 @@ val split_fix :
   int -> constr_expr -> constr_expr ->
   local_binder_expr list *  constr_expr * constr_expr
 
-val prec_less : int -> int * Ppextend.parenRelation -> bool
+val prec_less : precedence -> tolerability -> bool
 
 val pr_tight_coma : unit -> Pp.t
 
-- 
cgit v1.2.3