From 3b766fd8859b692e3e93cf83bf87d393e32c572e Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 3 Sep 2020 13:26:00 +0200
Subject: Merge numeral and string notation plugins

---
 plugins/syntax/string_notation.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'plugins/syntax/string_notation.ml')

diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml
index dbb0e92d5c..98ea318c92 100644
--- a/plugins/syntax/string_notation.ml
+++ b/plugins/syntax/string_notation.ml
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Pp
-open Util
 open Names
 open Libnames
 open Constrexpr
-- 
cgit v1.2.3