More monomorphic List.mem + List.assoc + ...

 To reduce the amount of syntactic noise, we now provide
 a few inner modules Int.List, Id.List, String.List, Sorts.List
 which contain some monomorphic (or semi-monomorphic) functions
 such as mem, assoc, ...

 NB: for Int.List.mem and co we reuse List.memq and so on.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16936 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 9 deletions

diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
index b74faf30b..4e9ca6ffc 100644
--- a/plugins/omega/omega.ml
+++ b/plugins/omega/omega.ml
@@ -546,30 +546,30 @@ let rec depend relie_on accu = function
   | act :: l ->
       begin match act with
 	| DIVIDE_AND_APPROX (e,_,_,_) ->
-            if List.mem e.id relie_on then depend relie_on (act::accu) l
+            if Int.List.mem e.id relie_on then depend relie_on (act::accu) l
             else depend relie_on accu l
 	| EXACT_DIVIDE (e,_) ->
-            if List.mem e.id relie_on then depend relie_on (act::accu) l
+            if Int.List.mem e.id relie_on then depend relie_on (act::accu) l
             else depend relie_on accu l
 	| WEAKEN (e,_) ->
-            if List.mem e relie_on then depend relie_on (act::accu) l
+            if Int.List.mem e relie_on then depend relie_on (act::accu) l
             else depend relie_on accu l
 	| SUM (e,(_,e1),(_,e2)) ->
-            if List.mem e relie_on then
+            if Int.List.mem e relie_on then
 	      depend (e1.id::e2.id::relie_on) (act::accu) l
             else
 	      depend relie_on accu l
 	| STATE {st_new_eq=e;st_orig=o} ->
-            if List.mem e.id relie_on then depend (o.id::relie_on) (act::accu) l
+            if Int.List.mem e.id relie_on then depend (o.id::relie_on) (act::accu) l
             else depend relie_on accu l
 	| HYP e ->
-            if List.mem e.id relie_on then depend relie_on (act::accu) l
+            if Int.List.mem e.id relie_on then depend relie_on (act::accu) l
             else depend relie_on accu l
 	| FORGET_C _ -> depend relie_on accu l
 	| FORGET _ -> depend relie_on accu l
 	| FORGET_I _ -> depend relie_on accu l
 	| MERGE_EQ (e,e1,e2) ->
-            if List.mem e relie_on then
+            if Int.List.mem e relie_on then
 	      depend (e1.id::e2::relie_on) (act::accu) l
             else
 	      depend relie_on accu l
@@ -673,7 +673,7 @@ let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system =
            try let _ = loop2 sys in raise NO_CONTRADICTION
            with UNSOLVABLE ->
              let relie_on,path = depend [] [] (history ()) in
-             let dc,_ = List.partition (fun (_,id,_) -> List.mem id relie_on) decomp in
+             let dc,_ = List.partition (fun (_,id,_) -> Int.List.mem id relie_on) decomp in
              let red = List.map (fun (x,_,_) -> x) dc in
              (red,relie_on,decomp,path))
         sys_exploded
@@ -705,7 +705,7 @@ let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system =
         let s2' = List.map remove_int s2 in
         let (r1,relie1) = solve s1'
 	and (r2,relie2) = solve s2' in
-	let (eq,id1,id2) = Util.List.assoc_f Int.equal id explode_map in
+	let (eq,id1,id2) = Int.List.assoc id explode_map in
 	[SPLIT_INEQ(eq,(id1,r1),(id2, r2))],
         eq.id :: Util.List.union Int.equal relie1 relie2
       with FULL_SOLUTION (x0,x1) -> (x0,x1)