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

(limited to 'printing/ppconstr.ml')

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index ee03bc9007..4a103cdd23 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -15,6 +15,7 @@ open Nameops
 open Libnames
 open Pputils
 open Ppextend
+open Notation_term
 open Constrexpr
 open Constrexpr_ops
 open Decl_kinds
@@ -737,7 +738,7 @@ let tag_var = tag Tag.variable
     pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t
   }
 
-  type precedence =  Ppextend.precedence * Ppextend.parenRelation
+  type precedence =  Notation_term.precedence * Notation_term.parenRelation
   let modular_constr_pr = pr
   let rec fix rf x = rf (fix rf) x
   let pr = fix modular_constr_pr mt
-- 
cgit v1.2.3