From 7c044bd9b5bca4970f6a936d5b6d5484bcb79397 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 24 Mar 2015 16:01:03 +0100
Subject: Fixing equality of notation_constrs. Fixes bug #4136.

---
 pretyping/glob_ops.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 67f3cb4169..e514fd529e 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -13,6 +13,9 @@ open Glob_term
 
 val cases_pattern_eq : cases_pattern -> cases_pattern -> bool
 
+val cast_type_eq : ('a -> 'a -> bool) ->
+  'a Misctypes.cast_type -> 'a Misctypes.cast_type -> bool
+
 val glob_constr_eq : glob_constr -> glob_constr -> bool
 
 (** Operations on [glob_constr] *)
-- 
cgit v1.2.3