From ef42739eadeb6ec3fc98b5beaa13bd859de44d15 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 23 Oct 2013 22:17:11 +0000
Subject: cList.index is now cList.index_f, same for index0

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16921 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/extraction/table.ml  | 2 +-
 plugins/funind/indfun.ml     | 2 +-
 plugins/romega/refl_omega.ml | 8 ++++----
 3 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 4e60696a81..ba21c6cbf1 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -656,7 +656,7 @@ let add_implicits r l =
 	else err (int i ++ str " is not a valid argument number for " ++
 		  safe_pr_global r)
     | ArgId id ->
-	(try List.index (Name id) names
+	(try List.index Name.equal (Name id) names
 	 with Not_found ->
 	   err (str "No argument " ++ pr_id id ++ str " for " ++
 		safe_pr_global r))
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 34b3728603..34814c350e 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -379,7 +379,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
 	if Int.equal (List.length names) 1 then 1
 	else error "Recursive argument must be specified"
       | Some wf_arg ->
-	  List.index (Name wf_arg) names
+	  List.index Name.equal (Name wf_arg) names
   in
   let unbounded_eq =
     let f_app_args =
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 752fa45984..860a2524c2 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -223,7 +223,7 @@ let unintern_omega env id =
    calcul des variables utiles. *)
 
 let add_reified_atom t env =
-  try List.index0_f Term.eq_constr t env.terms
+  try List.index0 Term.eq_constr t env.terms
   with Not_found ->
     let i = List.length env.terms in
     env.terms <- env.terms @ [t]; i
@@ -234,7 +234,7 @@ let get_reified_atom env =
 (* \subsection{Gestion de l'environnement de proposition pour Omega} *)
 (* ajout d'une proposition *)
 let add_prop env t =
-  try List.index0_f Term.eq_constr t env.props
+  try List.index0 Term.eq_constr t env.props
   with Not_found ->
     let i = List.length env.props in  env.props <- env.props @ [t]; i
 
@@ -1039,7 +1039,7 @@ let mk_direction_list l =
 (* \section{Rejouer l'historique} *)
 
 let get_hyp env_hyp i =
-  try List.index0 (CCEqua i) env_hyp
+  try List.index0 Pervasives.(=) (CCEqua i) env_hyp
   with Not_found -> failwith (Printf.sprintf "get_hyp %d" i)
 
 let replay_history env env_hyp =
@@ -1265,7 +1265,7 @@ let resolution env full_reified_goal systems_list =
       |	((O_left | O_mono) :: l) -> app coq_p_left [| loop l |]
       |	(O_right :: l) -> app coq_p_right [| loop l |] in
     let correct_index =
-      let i = List.index0 e.e_origin.o_hyp l_hyps in
+      let i = List.index0 Names.Id.equal e.e_origin.o_hyp l_hyps in
       (* PL: it seems that additionnally introduced hyps are in the way during
              normalization, hence this index shifting... *)
       if Int.equal i 0 then 0 else Pervasives.(+) i (List.length to_introduce)
-- 
cgit v1.2.3