From 7c1b36356c14b2571b5cb559d09586839703c660 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 19 Dec 2018 11:50:18 +0100
Subject: Fixing printing bug due to using equality ill-checking hash key of
 kernel name.

Thanks to Georges Gonthier for noticing it.

Expanding a few Pervasives.compare at this occasion.
---
 interp/notation.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'interp/notation.mli')

diff --git a/interp/notation.mli b/interp/notation.mli
index 75034cad70..a482e00e81 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -210,6 +210,8 @@ 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