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/constrextern.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 488c9a740f..717c476526 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -67,7 +67,10 @@ let print_no_symbol = ref false
 
 (**********************************************************************)
 (* Turning notations and scopes on and off for printing *)
-module IRuleSet = InterpRuleSet
+module IRuleSet = Set.Make(struct
+    type t = interp_rule
+    let compare x y = Pervasives.compare x y
+  end)
 
 let inactive_notations_table =
   Summary.ref ~name:"inactive_notations_table" (IRuleSet.empty)
-- 
cgit v1.2.3