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

16 files changed, 35 insertions, 39 deletions

diff --git a/checker/closure.ml b/checker/closure.ml
index 55c91b93e..38527249c 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -357,7 +357,7 @@ let rec compact_constr (lg, subs as s) c k =
   match c with
       Rel i ->
         if i < k then c,s else
-          (try Rel (k + lg - List.index (i-k+1) subs), (lg,subs)
+          (try Rel (k + lg - List.index Int.equal (i-k+1) subs), (lg,subs)
           with Not_found -> Rel (k+lg), (lg+1, (i-k+1)::subs))
     | (Sort _|Var _|Meta _|Ind _|Const _|Construct _) -> c,s
     | Evar(ev,v) ->
diff --git a/ide/wg_Notebook.ml b/ide/wg_Notebook.ml
index 76d6cbed9..51e628c8f 100644
--- a/ide/wg_Notebook.ml
+++ b/ide/wg_Notebook.ml
@@ -46,7 +46,7 @@ object(self)
     List.nth term_list i
 
   method term_num f p =
-    Util.List.index0_f f p term_list
+    Util.List.index0 f p term_list
 
   method pages = term_list
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 74a49152c..2c44d6da3 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1334,7 +1334,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
         let lf = List.map (fun ((_, id),_,_,_,_) -> id) dl in
         let dl = Array.of_list dl in
 	let n =
-	  try List.index0 iddef lf
+	  try List.index0 Id.equal iddef lf
           with Not_found ->
 	    raise (InternalizationError (locid,UnboundFixName (false,iddef)))
 	in
@@ -1375,7 +1375,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
         let lf = List.map (fun ((_, id),_,_,_) -> id) dl in
         let dl = Array.of_list dl in
 	let n =
-          try List.index0 iddef lf
+          try List.index0 Id.equal iddef lf
           with Not_found ->
 	    raise (InternalizationError (locid,UnboundFixName (true,iddef)))
 	in
diff --git a/kernel/closure.ml b/kernel/closure.ml
index faa67be46..28818de1f 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -483,7 +483,7 @@ let rec compact_constr (lg, subs as s) c k =
   match kind_of_term c with
       Rel i ->
         if i < k then c,s else
-          (try mkRel (k + lg - List.index (i-k+1) subs), (lg,subs)
+          (try mkRel (k + lg - List.index Int.equal (i-k+1) subs), (lg,subs)
           with Not_found -> mkRel (k+lg), (lg+1, (i-k+1)::subs))
     | (Sort _|Var _|Meta _|Ind _|Const _|Construct _) -> c,s
     | Evar(ev,v) ->
diff --git a/lib/cList.ml b/lib/cList.ml
index 904f3ee63..a6d157291 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -90,10 +90,8 @@ sig
   val filteri :
     (int -> 'a -> bool) -> 'a list -> 'a list
   val smartfilter : ('a -> bool) -> 'a list -> 'a list
-  val index : 'a -> 'a list -> int
-  val index_f : ('a -> 'a -> bool) -> 'a -> 'a list -> int
-  val index0 : 'a -> 'a list -> int
-  val index0_f : ('a -> 'a -> bool) -> 'a -> 'a list -> int
+  val index : 'a eq -> 'a -> 'a list -> int
+  val index0 : 'a eq -> 'a -> 'a list -> int
   val iteri :  (int -> 'a -> unit) -> 'a list -> unit
   val fold_left_until : ('c -> 'a -> 'c CSig.until) -> 'c -> 'a list -> 'c
   val fold_right_i :  (int -> 'a -> 'b -> 'b) -> int -> 'a list -> 'b -> 'b
@@ -406,18 +404,14 @@ let rec smartfilter f l = match l with
           else h :: tl'
         else tl'
 
-let index_f f x =
+let index f x =
   let rec index_x n = function
     | y::l -> if f x y then n else index_x (succ n) l
     | [] -> raise Not_found
   in
   index_x 1
 
-let index0_f f x l = index_f f x l - 1
-
-let index x l = index_f Pervasives.(=) x l (* FIXME : prefer [index_f]*)
-
-let index0 x l = index x l - 1 (* FIXME *)
+let index0 f x l = index f x l - 1
 
 let fold_left_until f accu s =
   let rec aux accu = function
diff --git a/lib/cList.mli b/lib/cList.mli
index ee6595632..aec326c51 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -137,16 +137,12 @@ sig
   (** [smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i
     [f ai = true], then [smartfilter f l == l] *)
 
-  val index : 'a -> 'a list -> int
+  val index : 'a eq -> 'a -> 'a list -> int
   (** [index] returns the 1st index of an element in a list (counting from 1). *)
 
-  val index_f : 'a eq -> 'a -> 'a list -> int
-
-  val index0 : 'a -> 'a list -> int
+  val index0 : 'a eq -> 'a -> 'a list -> int
   (** [index0] behaves as [index] except that it starts counting at 0. *)
 
-  val index0_f : 'a eq -> 'a -> 'a list -> int
-
   val iteri :  (int -> 'a -> unit) -> 'a list -> unit
   (** As [iter] but with the index argument (starting from 0). *)
 
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 13e422b54..b72bb0264 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -114,7 +114,7 @@ let mk_fix_tac (loc,id,bl,ann,ty) =
         [([_],_,_)], None -> 1
       | _, Some x ->
           let ids = List.map snd (List.flatten (List.map pi1 bl)) in
-          (try List.index (snd x) ids
+          (try List.index Names.Name.equal (snd x) ids
           with Not_found -> error "No such fix variable.")
       | _ -> error "Cannot guess decreasing argument of fix." in
   (id,n,CProdN(loc,bl,ty))
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 4e60696a8..ba21c6cbf 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 34b372860..34814c350 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 752fa4598..860a2524c 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)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 7ab2a27ca..bdbfe412e 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -219,7 +219,7 @@ let lookup_index_as_renamed env t n =
 
 let update_name na ((_,e),c) =
   match na with
-  | Name _ when force_wildcard () && noccurn (List.index na e) c ->
+  | Name _ when force_wildcard () && noccurn (List.index Name.equal na e) c ->
       Anonymous
   | _ ->
       na
@@ -249,7 +249,8 @@ and align_tree nal isgoal (e,c as rhs) = match nal with
   | [] -> [[],rhs]
   | na::nal ->
     match kind_of_term c with
-    | Case (ci,p,c,cl) when eq_constr c (mkRel (List.index na (snd e)))
+    | Case (ci,p,c,cl) when
+        eq_constr c (mkRel (List.index Name.equal na (snd e)))
 	&& (* don't contract if p dependent *)
 	computable p (ci.ci_pp_info.ind_nargs) ->
 	let clauses = build_tree na isgoal e ci cl in
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 16a9c8a32..8e77de9c5 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -112,7 +112,7 @@ let dummy_constr = mkProp
 let make_renaming ids = function
 | (Name id, Name _, _) ->
   begin
-    try mkRel (List.index id ids)
+    try mkRel (List.index Id.equal id ids)
     with Not_found -> dummy_constr
   end
 | _ -> dummy_constr
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 329af8526..79e3913a9 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -206,7 +206,10 @@ let instantiate_pattern sigma lvar c =
 	let ctx,c = Id.Map.find id lvar in
 	try
 	  let inst =
-	    List.map (fun id -> mkRel (List.index (Name id) vars)) ctx in
+	    List.map
+              (fun id -> mkRel (List.index Name.equal (Name id) vars))
+              ctx
+          in
 	  let c = substl inst c in
 	  snd (pattern_of_constr sigma c)
 	with Not_found (* List.index failed *) ->
@@ -301,7 +304,7 @@ let err loc pp = user_err_loc (loc,"pattern_of_glob_constr", pp)
 
 let rec pat_of_raw metas vars = function
   | GVar (_,id) ->
-      (try PRel (List.index (Name id) vars)
+      (try PRel (List.index Name.equal (Name id) vars)
        with Not_found -> PVar id)
   | GPatVar (_,(false,n)) ->
       metas := n::!metas; PMeta (Some n)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 6e64e3fa6..1db40e8db 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -329,7 +329,7 @@ let make_elim_fun (names,(nbfix,lv,n)) largs =
   let la =
     List.map_i (fun q aq ->
       (* k from the comment is q+1 *)
-      try mkRel (p+1-(List.index (n-q) lyi))
+      try mkRel (p+1-(List.index Int.equal (n-q) lyi))
       with Not_found -> aq)
       0 (List.map (lift p) lu)
   in
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 231f764c5..97e50aadb 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -479,11 +479,13 @@ let check_open_binder isopen sl m =
 
 (* Heuristics for building default printing rules *)
 
+let index_id id l = List.index Id.equal id l
+
 let make_hunks etyps symbols from =
   let vars,typs = List.split etyps in
   let rec make = function
     | NonTerminal m :: prods ->
-	let i = List.index m vars in
+	let i = index_id m vars in
 	let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in
 	let u = UnpMetaVar (i,prec) in
 	if is_next_non_terminal prods then
@@ -516,7 +518,7 @@ let make_hunks etyps symbols from =
 	add_break n (make prods)
 
     | SProdList (m,sl) :: prods ->
-	let i = List.index m vars in
+	let i = index_id m vars in
 	let typ = List.nth typs (i-1) in
 	let _,prec = precedence_of_entry_type from typ in
         let sl' =
@@ -604,7 +606,7 @@ let hunks_of_format (from,(vars,typs)) symfmt =
       when String.equal s (String.drop_simple_quotes s') ->
       let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l
   | NonTerminal s :: symbs, UnpTerminal s' :: fmt when Id.equal s (Id.of_string s') ->
-      let i = List.index s vars in
+      let i = index_id s vars in
       let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in
       let symbs, l = aux (symbs,fmt) in symbs, UnpMetaVar (i,prec) :: l
   | symbs, UnpBox (a,b) :: fmt ->
@@ -614,7 +616,7 @@ let hunks_of_format (from,(vars,typs)) symfmt =
   | symbs, (UnpCut _ as u) :: fmt ->
       let symbs, l = aux (symbs,fmt) in symbs, u :: l
   | SProdList (m,sl) :: symbs, fmt ->
-      let i = List.index m vars in
+      let i = index_id m vars in
       let typ = List.nth typs (i-1) in
       let _,prec = precedence_of_entry_type from typ in
       let slfmt,fmt = read_recursive_format sl fmt in
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 3c4b88f46..0a21b6d6e 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -108,7 +108,7 @@ let subst_evar_constr evs n idf t =
 (** Substitute variable references in t using De Bruijn indices,
   where n binders were passed through. *)
 let subst_vars acc n t =
-  let var_index id = Util.List.index id acc in
+  let var_index id = Util.List.index Id.equal id acc in
   let rec substrec depth c = match kind_of_term c with
     | Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c)
     | _ -> map_constr_with_binders succ substrec depth c