cList: a few alternative to hashtbl-based uniquize, distinct, subset

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

4 files changed, 15 insertions, 8 deletions

diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index bf07156f73..67c5ba92fa 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -369,8 +369,8 @@ let get_common_underlying_mutual_inductive = function
       | (_,ind')::_ ->
 	  raise (RecursionSchemeError (NotMutualInScheme (ind,ind')))
       | [] ->
-	  if not (List.distinct (List.map snd (List.map snd all))) then
-	    error "A type occurs twice";
+	  if not (List.distinct_f Int.compare (List.map snd (List.map snd all)))
+          then error "A type occurs twice";
 	  mind,
 	  List.map_filter
 	    (function (Some id,(_,i)) -> Some (i,snd id) | (None,_) -> None) all
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index a25f96d469..519112dfdb 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -135,8 +135,13 @@ let find_mutually_recursive_statements thms =
       | [], _::_ ->
           let () = match same_indccl with
           | ind :: _ ->
-            if List.distinct (List.map pi1 ind) then
-              if_verbose msg_info (strbrk "Coinductive statements do not follow the order of definition, assuming the proof to be by induction."); flush_all ()
+            if List.distinct_f ind_ord (List.map pi1 ind)
+            then
+              if_verbose msg_info
+                (strbrk
+                   ("Coinductive statements do not follow the order of "^
+                    "definition, assuming the proof to be by induction."));
+            flush_all ()
           | _ -> ()
           in
           let possible_guards = List.map (List.map pi3) inds_hyps in
diff --git a/toplevel/record.ml b/toplevel/record.ml
index e0dc6c3a3f..cf57145465 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -376,7 +376,8 @@ let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuil
     | Vernacexpr.DefExpr ((_,Name id),_,_) -> id::acc
     | _ -> acc in
   let allnames =  idstruc::(List.fold_left extract_name [] fs) in
-  if not (List.distinct allnames) then error "Two objects have the same name";
+  if not (List.distinct_f Id.compare allnames)
+  then error "Two objects have the same name";
   let isnot_class = match kind with Class false -> false | _ -> true in
   if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then
     error "Priorities only allowed for type class substructures";
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index fd4ac48907..3c104f543f 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -802,7 +802,8 @@ let vernac_set_end_tac tac =
 
 let vernac_set_used_variables l =
   let l = List.map snd l in
-  if not (List.distinct l) then error "Used variables list contains duplicates";
+  if not (List.distinct_f Id.compare l)
+  then error "Used variables list contains duplicates";
   let vars = Environ.named_context (Global.env ()) in
   List.iter (fun id -> 
     if not (List.exists (fun (id',_,_) -> Id.equal id id') vars) then
@@ -898,8 +899,8 @@ let vernac_declare_arguments locality r l nargs flags =
   let scopes = List.map (List.map (fun (_,_, s, _,_) -> s)) l in
   if List.exists (fun na -> not (List.equal Name.equal na names)) rest then
     error "All arguments lists must declare the same names.";
-  if not (List.distinct (List.filter ((!=) Anonymous) names)) then
-    error "Arguments names must be distinct.";
+  if not (List.distinct_f Name.compare (List.filter ((!=) Anonymous) names))
+  then error "Arguments names must be distinct.";
   let sr = smart_global r in
   let inf_names =
     Impargs.compute_implicits_names (Global.env()) (Global.type_of_global sr) in