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

4 files changed, 8 insertions, 5 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 373a0bb62e..6050fdc9a7 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1352,7 +1352,7 @@ and trivial_resolve dbg mod_delta db_list local_db cl =
 
 let make_db_list dbnames =
   let use_core = not (List.mem "nocore" dbnames) in
-  let dbnames = List.remove "nocore" dbnames in
+  let dbnames = List.remove String.equal "nocore" dbnames in
   let dbnames = if use_core then "core"::dbnames else dbnames in
   let lookup db =
     try searchtable_map db with Not_found -> error_no_such_hint_database db
diff --git a/tactics/equality.ml b/tactics/equality.ml
index f5af80b0d5..9bc86a0b97 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -430,7 +430,7 @@ let general_multi_rewrite l2r with_evars ?tac c cl =
 	  (* If the term to rewrite uses an hypothesis H, don't rewrite in H *)
 	  let ids =
 	    let ids_in_c = Environ.global_vars_set (Global.env()) (fst c) in
-	      Id.Set.fold (fun id l -> List.remove id l) ids_in_c (pf_ids_of_hyps gl)
+	      Id.Set.fold (fun id l -> List.remove Id.equal id l) ids_in_c (pf_ids_of_hyps gl)
 	  in do_hyps_atleastonce ids gl
 	in
 	if cl.concl_occs == NoOccurrences then do_hyps else
@@ -565,7 +565,9 @@ let find_positions env sigma t1 t2 =
       | Construct sp1, Construct sp2
           when Int.equal (List.length args1) (mis_constructor_nargs_env env sp1)
             ->
-	  let sorts = List.intersect sorts (allowed_sorts env (fst sp1)) in
+	  let sorts =
+            List.intersect Sorts.family_equal sorts (allowed_sorts env (fst sp1))
+          in
           (* both sides are fully applied constructors, so either we descend,
              or we can discriminate here. *)
 	  if is_conv env sigma hd1 hd2 then
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 2a00f7defd..190c1ba58e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1393,7 +1393,8 @@ and apply_hyps_context ist env lz goal mt lctxt lgmatch mhyps hyps =
           db_matched_hyp (curr_debug ist) (pf_env goal) hyp_match hypname;
 	  try
             let id_match = pi1 hyp_match in
-            let nextlhyps = List.remove_assoc_in_triple id_match lhyps_rest in
+            let select_match (id,_,_) = Id.equal id id_match in
+            let nextlhyps = List.remove_first select_match lhyps_rest in
             let lfun = lfun +++ lids in
             apply_hyps_context_rec lfun s.e_sub nextlhyps tl
           with e when is_match_catchable e ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 298d26915f..2505a43ad9 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -889,7 +889,7 @@ let clenv_fchain_in id ?(flags=elim_flags) mv elimclause hypclause =
 let elimination_in_clause_scheme with_evars ?(flags=elim_flags) id i elimclause indclause gl =
   let indmv = destMeta (nth_arg i elimclause.templval.rebus) in
   let hypmv =
-    try match List.remove indmv (clenv_independent elimclause) with
+    try match List.remove Int.equal indmv (clenv_independent elimclause) with
       | [a] -> a
       | _ -> failwith ""
     with Failure _ -> errorlabstrm "elimination_clause"