From 3d5b210d4148e1edb9f7a02c888decf9cc6c30e6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 21 Jul 2015 11:03:55 +0200
Subject: Fixing bug #4303: Anomaly: Uncaught exception Invalid_argument.

---
 pretyping/miscops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index a2c97d2cb1..0926e7a299 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -30,7 +30,7 @@ let smartmap_cast_type f c =
 let glob_sort_eq g1 g2 = match g1, g2 with
 | GProp, GProp -> true
 | GSet, GSet -> true
-| GType l1, GType l2 -> List.for_all2 CString.equal l1 l2
+| GType l1, GType l2 -> List.equal CString.equal l1 l2
 | _ -> false
 
 let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with
-- 
cgit v1.2.3