From 2c18da20b260c55d8da49b1bb4f53e72dbc75a87 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Wed, 24 Apr 2019 11:37:42 +0000
Subject: Revert #9249

---
 interp/notation.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'interp/notation.mli')

diff --git a/interp/notation.mli b/interp/notation.mli
index 57e2be16b9..017023c133 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -216,8 +216,6 @@ type interp_rule =
   | NotationRule of scope_name option * notation
   | SynDefRule of KerName.t
 
-module InterpRuleSet : Set.S with type elt = interp_rule
-
 val declare_notation_interpretation : notation -> scope_name option ->
       interpretation -> notation_location -> onlyprint:bool -> unit
 
-- 
cgit v1.2.3