From 87b510e5b0f363724eae5db9f177f167a3586015 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 1 Mar 2014 18:26:26 +0100
Subject: Fixing pervasive comparisons

---
 proofs/clenv.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index a8bbfe127e..966d247e0e 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -378,8 +378,13 @@ let clenv_independent clenv =
   let deps = Metaset.union (dependent_in_type_of_metas clenv mvs) ctyp_mvs in
   List.filter (fun mv -> not (Metaset.mem mv deps)) mvs
 
+let qhyp_eq h1 h2 = match h1, h2 with
+| NamedHyp n1, NamedHyp n2 -> Id.equal n1 n2
+| AnonHyp i1, AnonHyp i2 -> Int.equal i1 i2
+| _ -> false
+
 let check_bindings bl =
-  match List.duplicates Pervasives.(=) (List.map pi2 bl) with (* FIXME *)
+  match List.duplicates qhyp_eq (List.map pi2 bl) with
     | NamedHyp s :: _ ->
 	errorlabstrm ""
 	  (str "The variable " ++ pr_id s ++
-- 
cgit v1.2.3