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

(limited to 'API/API.ml')

diff --git a/API/API.ml b/API/API.ml
index 1d7a4a4f46..c4bcef6f6c 100644
--- a/API/API.ml
+++ b/API/API.ml
@@ -169,7 +169,6 @@ module Stdarg = Stdarg
 module Genintern = Genintern
 module Constrexpr_ops = Constrexpr_ops
 module Notation_ops = Notation_ops
-module Ppextend = Ppextend
 module Notation = Notation
 module Dumpglob = Dumpglob
 (* module Syntax_def *)
-- 
cgit v1.2.3