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 -
 1 file changed, 1 deletion(-)

(limited to 'interp/notation.ml')

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
 
-- 
cgit v1.2.3