From 5e6145c871eea1e94566b252b4bfc4cd752f42d5 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 23 Oct 2013 22:17:07 +0000
Subject: cList: set-as-list functions are now with an explicit comparison

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16920 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/romega/refl_omega.ml | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

(limited to 'plugins/romega')

diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 635fc366f3..752fa45984 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -921,7 +921,7 @@ let add_stated_equations env tree =
 let rec get_eclatement env = function
     i :: r ->
       let l = try (get_equation env i).e_depends with Not_found -> [] in
-      List.union (List.rev l) (get_eclatement env r)
+      List.union Pervasives.(=) (List.rev l) (get_eclatement env r)
   | [] -> []
 
 let select_smaller l =
@@ -1207,12 +1207,16 @@ let resolution env full_reified_goal systems_list =
   (* recupere explicitement ces equations *)
   let equations = List.map (get_equation env) useful_equa_id in
   let l_hyps' = List.uniquize (List.map (fun e -> e.e_origin.o_hyp) equations) in
-  let l_hyps = id_concl :: List.remove id_concl l_hyps' in
+  let l_hyps = id_concl :: List.remove Names.Id.equal id_concl l_hyps' in
   let useful_hyps =
-    List.map (fun id -> List.assoc id full_reified_goal) l_hyps in
+    List.map
+      (fun id -> List.assoc_f Names.Id.equal id full_reified_goal) l_hyps
+  in
   let useful_vars =
     let really_useful_vars = vars_of_equations equations in
-    let concl_vars = vars_of_prop (List.assoc id_concl full_reified_goal) in
+    let concl_vars =
+      vars_of_prop (List.assoc_f Names.Id.equal id_concl full_reified_goal)
+    in
     really_useful_vars @@ concl_vars
   in
   (* variables a introduire *)
-- 
cgit v1.2.3