Slight cleanup of refl_omega.ml : in particular it uses now list

utilities from Util. Some additions in Util, and simplifications 
in various files. 



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

10 files changed, 103 insertions, 126 deletions

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index dc1dc2cfb..0fa73f096 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -516,7 +516,7 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp
 			 (Topconstr.names_of_local_assums args) 
 		     in 
 		     let annot = 
-		       try Some (list_index (Name id) names - 1), Topconstr.CStructRec 
+		       try Some (list_index0 (Name id) names), Topconstr.CStructRec 
 		       with Not_found -> 
 			 raise (UserError("",str "Cannot find argument " ++ 
 					    Ppconstr.pr_id id)) 
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
index 169542e3c..b6398a329 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/indfun_main.ml4
@@ -169,7 +169,7 @@ VERNAC ARGUMENT EXTEND rec_definition2
 	   | Struct id -> id | Wf(_,Some id,_) -> id | Mes(_,Some id,_) -> id 
 	   | Wf(_,None,_) | Mes(_,None,_) -> failwith "check_exists_args" 
 	 in 
-	 (try ignore(Util.list_index (Name id) names - 1); annot
+	 (try ignore(Util.list_index0 (Name id) names); annot
 	  with Not_found ->  Util.user_err_loc
             (Util.dummy_loc,"Function",
              Pp.str "No argument named " ++ Nameops.pr_id id)
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index b78aa9845..5fcd04c46 100644
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -242,9 +242,6 @@ module MySearchProblem = struct
 	with e when Logic.catchable_exception e ->
 	  filter_tactics (glls,v) tacl
 
-  let rec list_addn n x l = 
-    if n = 0 then l else x :: (list_addn (pred n) x l)
-
   (* Ordering of states is lexicographic on depth (greatest first) then
      number of remaining goals. *)
   let compare s s' =
diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml
index e7e7b3c59..7c99f7e14 100644
--- a/contrib/romega/refl_omega.ml
+++ b/contrib/romega/refl_omega.ml
@@ -6,10 +6,7 @@
 
  *************************************************************************)
 
-(* The addition on int, since it while be hidden soon by the one on BigInt *)
-
-let (+.) = (+)
-
+open Util
 open Const_omega
 module OmegaSolver = Omega.MakeOmegaSolver (Bigint)
 open OmegaSolver
@@ -26,65 +23,6 @@ let pp i = print_int i; print_newline (); flush stdout
 (* More readable than the prefix notation *)
 let (>>) = Tacticals.tclTHEN
 
-(* [list_index t l = i] \eqv $nth l i = t \wedge \forall j < i nth l j != t$ *)
-
-let list_index t = 
-  let rec loop i = function
-    | (u::l) -> if u = t then i else loop (succ i) l
-    | [] -> raise Not_found in
-  loop 0
-
-(* [list_uniq l = filter_i (x i -> nth l (i-1) != x) l] *)
-let list_uniq l  = 
-  let rec uniq = function
-      x :: ((y :: _) as l) when x = y -> uniq l
-    | x :: l -> x :: uniq l
-    | [] -> [] in
-  uniq (List.sort compare l)
-
-(* $\forall x. mem x  (list\_union l1 l2) \eqv x \in \{l1\} \cup \{l2\}$ *)
-let list_union l1 l2 =
-  let rec loop buf = function
-      x :: r -> if List.mem x l2 then loop buf r else loop (x :: buf) r
-    | [] -> buf in
-  loop l2 l1
-
-(* $\forall x. 
-      mem \;\; x \;\; (list\_intersect\;\; l1\;\;l2) \eqv x \in \{l1\} 
-       \cap \{l2\}$ *)
-let list_intersect l1 l2 =
-  let rec loop buf = function
-      x :: r -> if List.mem x l2 then loop (x::buf) r else loop buf r
-    | [] -> buf in
-  loop [] l1
-
-(* cartesian product. Elements are lists and are concatenated.
-   $cartesian [x_1 ... x_n] [y_1 ... y_p] = [x_1 @ y_1, x_2 @ y_1 ... x_n @ y_1 , x_1 @ y_2 ... x_n @ y_p]$ *)
-
-let rec cartesien l1 l2 =
-  let rec loop = function
-      (x2 :: r2) -> List.map (fun x1 -> x1 @ x2) l1 @ loop r2
-    | [] -> [] in
-  loop l2
-
-(* remove element e from list l *)
-let list_remove e l =
-  let rec loop = function
-      x :: l -> if x = e then loop l else x :: loop l
-    | [] -> [] in
-  loop l
-
-(* equivalent of the map function but no element is added when the function
-   raises an exception (and the computation silently continues) *)
-let map_exc f = 
-  let rec loop = function 
-    (x::l) -> 
-      begin match try Some (f x) with exc -> None with
-        Some v -> v :: loop l | None -> loop l
-      end
-    | [] -> [] in
-  loop 
-
 let mkApp = Term.mkApp
 
 (* \section{Types}
@@ -174,6 +112,7 @@ type environment = {
 (* \subsection{Solution tree}
    Définition d'une solution trouvée par Omega sous la forme d'un identifiant,
    d'un ensemble d'équation dont dépend la solution et d'une trace *)
+(* La liste des dépendances est triée et sans redondance *)
 type solution = {
   s_index : int;
   s_equa_deps : int list;
@@ -280,7 +219,7 @@ let unintern_omega env id =
    calcul des variables utiles. *)
 
 let add_reified_atom t env =
-  try list_index t env.terms
+  try list_index0 t env.terms
   with Not_found ->
     let i = List.length env.terms in
     env.terms <- env.terms @ [t]; i
@@ -291,7 +230,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_index t env.props
+  try list_index0 t env.props
   with Not_found ->
     let i = List.length env.props in  env.props <- env.props @ [t]; i
 
@@ -469,22 +408,34 @@ Ces fonctions préparent les traces utilisées par la tactique réfléchie
 pour faire des opérations de normalisation sur les équations.  *)
 
 (* \subsection{Extractions des variables d'une équation} *)
-(* Extraction des variables d'une équation *)
+(* Extraction des variables d'une équation. *)
+(* Chaque fonction retourne une liste triée sans redondance *)
+
+let (@@) = list_merge_uniq compare
 
 let rec vars_of_formula = function
   | Oint _ -> []
-  | Oplus (e1,e2)  -> (vars_of_formula e1) @ (vars_of_formula e2)
-  | Omult (e1,e2)  -> (vars_of_formula e1) @ (vars_of_formula e2)
-  | Ominus (e1,e2) -> (vars_of_formula e1) @ (vars_of_formula e2)
-  | Oopp e -> (vars_of_formula e)
+  | Oplus (e1,e2) -> (vars_of_formula e1) @@ (vars_of_formula e2)
+  | Omult (e1,e2) -> (vars_of_formula e1) @@ (vars_of_formula e2)
+  | Ominus (e1,e2) -> (vars_of_formula e1) @@ (vars_of_formula e2)
+  | Oopp e -> vars_of_formula e
   | Oatom i -> [i]
   | Oufo _ -> []
 
-let vars_of_equations l =
-  let rec loop = function
-      e :: l -> vars_of_formula e.e_left @ vars_of_formula e.e_right @ loop l
-    | [] -> [] in
-  list_uniq (List.sort compare (loop l))
+let rec vars_of_equations = function
+  | [] -> [] 
+  | e::l -> 
+      (vars_of_formula e.e_left) @@
+      (vars_of_formula e.e_right) @@
+      (vars_of_equations l)
+
+let rec vars_of_prop = function 
+  | Pequa(_,e) -> vars_of_equations [e]
+  | Pnot p -> vars_of_prop p
+  | Por(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2)
+  | Pand(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2)
+  | Pimp(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2)
+  | Pprop _ | Ptrue | Pfalse -> []
 
 (* \subsection{Multiplication par un scalaire} *)
 
@@ -881,7 +832,7 @@ let destructurate_hyps syst =
       (i,t) :: l -> 
 	let l_syst1 = destructurate_pos_hyp i []  [] t in
 	let l_syst2 = loop l in
-	cartesien l_syst1 l_syst2
+	list_cartesian (@) l_syst1 l_syst2
     | [] -> [[]] in
   loop syst
 
@@ -924,9 +875,9 @@ let display_systems syst_list =
 let rec hyps_used_in_trace = function
   | act :: l -> 
       begin match act with
-	| HYP e -> e.id :: hyps_used_in_trace l
+	| HYP e -> [e.id] @@ (hyps_used_in_trace l)
 	| SPLIT_INEQ (_,(_,act1),(_,act2)) -> 
-	    hyps_used_in_trace act1 @ hyps_used_in_trace act2
+	    hyps_used_in_trace act1 @@ hyps_used_in_trace act2
 	| _ -> hyps_used_in_trace l
       end
   | [] -> []
@@ -950,14 +901,15 @@ let rec variable_stated_in_trace = function
 ;;
 
 let add_stated_equations env tree = 
-  let rec loop = function
-      Tree(_,t1,t2) -> 
-	list_union (loop t1) (loop t2)
-    | Leaf s -> variable_stated_in_trace s.s_trace in
   (* Il faut trier les variables par ordre d'introduction pour ne pas risquer
      de définir dans le mauvais ordre *)
   let stated_equations = 
-    List.sort (fun x y -> Pervasives.(-) x.st_var y.st_var) (loop tree) in
+    let cmpvar x y = Pervasives.(-) x.st_var y.st_var in 
+    let rec loop = function
+      | Tree(_,t1,t2) -> List.merge cmpvar (loop t1) (loop t2)
+      | Leaf s -> List.sort cmpvar (variable_stated_in_trace s.s_trace) 
+    in loop tree
+  in 
   let add_env st = 
     (* On retransforme la définition de v en formule reifiée *)
     let v_def = oformula_of_omega env st.st_def in
@@ -978,10 +930,15 @@ let add_stated_equations env tree =
 (* Calcule la liste des éclatements à réaliser sur les hypothèses 
    nécessaires pour extraire une liste d'équations donnée *)
 
+(* PL: experimentally, the result order of the following function seems 
+   _very_ crucial for efficiency. No idea why. Do not remove the List.rev
+   or modify the current semantics of Util.list_union (some elements of first 
+   arg, then second arg), unless you know what you're doing. *)
+
 let rec get_eclatement env = function
     i :: r -> 
       let l = try (get_equation env i).e_depends with Not_found -> [] in
-      list_union l (get_eclatement env r)
+      list_union (List.rev l) (get_eclatement env r)
   | [] -> []
 
 let select_smaller l = 
@@ -992,14 +949,13 @@ let filter_compatible_systems required systems =
   let rec select = function
       (x::l) -> 
 	if List.mem x required then select l
-	else if List.mem (barre x) required then raise Exit 
+	else if List.mem (barre x) required then failwith "Exit" 
 	else x :: select l
     | [] -> [] in
-  map_exc (function (sol,splits) -> (sol,select splits)) systems
+  map_succeed (function (sol,splits) -> (sol,select splits)) systems
 
 let rec equas_of_solution_tree = function
-    Tree(_,t1,t2) -> 
-      list_union (equas_of_solution_tree t1) (equas_of_solution_tree t2)
+    Tree(_,t1,t2) -> (equas_of_solution_tree t1)@@(equas_of_solution_tree t2)
   | Leaf s -> s.s_equa_deps
 
 (* [really_useful_prop] pushes useless props in a new Pprop variable *)
@@ -1041,14 +997,6 @@ let really_useful_prop l_equa c =
     None -> Pprop (real_of c)
   | Some t -> t
 
-let rec vars_of_prop = function 
-  | Pequa(_,e) -> vars_of_equations [e]
-  | Pnot p -> vars_of_prop p
-  | Por(_,p1,p2) -> list_union (vars_of_prop p1) (vars_of_prop p2)
-  | Pand(_,p1,p2) -> list_union (vars_of_prop p1) (vars_of_prop p2)
-  | Pimp(_,p1,p2) -> list_union (vars_of_prop p1) (vars_of_prop p2)
-  | _ -> []
-
 let rec display_solution_tree ch = function
     Leaf t -> 
       output_string ch 
@@ -1103,7 +1051,7 @@ let mk_direction_list l =
 (* \section{Rejouer l'historique} *)
 
 let get_hyp env_hyp i =
-  try list_index (CCEqua i) env_hyp
+  try list_index0 (CCEqua i) env_hyp
   with Not_found -> failwith (Printf.sprintf "get_hyp %d" i)
 
 let replay_history env env_hyp =
@@ -1267,17 +1215,17 @@ let resolution env full_reified_goal systems_list =
     print_newline()
   end;
   (* calcule la liste de toutes les hypothèses utilisées dans l'arbre de solution *)
-  let useful_equa_id = list_uniq (equas_of_solution_tree solution_tree) in
+  let useful_equa_id = equas_of_solution_tree solution_tree in
   (* recupere explicitement ces equations *)
   let equations = List.map (get_equation env) useful_equa_id in
-  let l_hyps' = list_uniq (List.map (fun e -> e.e_origin.o_hyp) equations) in
+  let l_hyps' = list_uniquize (List.map (fun e -> e.e_origin.o_hyp) equations) in
   let l_hyps = id_concl :: list_remove id_concl l_hyps' in
   let useful_hyps =
     List.map (fun id -> List.assoc id full_reified_goal) l_hyps in
   let useful_vars = 
     let really_useful_vars = vars_of_equations equations in
     let concl_vars = vars_of_prop (List.assoc id_concl full_reified_goal) in     
-    list_uniq (List.sort compare (really_useful_vars @ concl_vars))
+    really_useful_vars @@ concl_vars
   in 
   (* variables a introduire *)
   let to_introduce = add_stated_equations env solution_tree in
@@ -1325,10 +1273,10 @@ 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_index e.e_origin.o_hyp l_hyps in 
+      let i = list_index0 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 i=0 then 0 else i +. List.length to_introduce
+      if i=0 then 0 else Pervasives.(+) i (List.length to_introduce)
     in 	
     app coq_pair_step [| mk_nat correct_index; loop e.e_origin.o_path |] in
   let normalization_trace =
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 2e5ec38c8..74ea5aef6 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -789,8 +789,7 @@ let internalise 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_index iddef lf) -1
+	  try list_index0 iddef lf
           with Not_found ->
 	    raise (InternalisationError (locid,UnboundFixName (false,iddef)))
 	in
@@ -827,8 +826,7 @@ let internalise 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_index iddef lf) -1
+          try list_index0 iddef lf
           with Not_found ->
 	    raise (InternalisationError (locid,UnboundFixName (true,iddef)))
 	in
diff --git a/lib/util.ml b/lib/util.ml
index 590d64993..7e59d1474 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -216,6 +216,8 @@ let list_index x =
   in 
   index_x 1
 
+let list_index0 x l = list_index x l - 1 
+
 let list_unique_index x = 
   let rec index_x n = function
     | y::l -> 
@@ -329,6 +331,18 @@ let rec list_distinct l =
     | [] -> true
   in loop l
 
+let rec list_merge_uniq cmp l1 l2 =
+  match l1, l2 with
+  | [], l2 -> l2
+  | l1, [] -> l1
+  | h1 :: t1, h2 :: t2 ->
+      let c = cmp h1 h2 in 
+      if c = 0 
+      then h1 :: list_merge_uniq cmp t1 t2
+      else if c <= 0 
+      then h1 :: list_merge_uniq cmp t1 l2
+      else h2 :: list_merge_uniq cmp l1 t2
+
 let rec list_duplicates = function
   | [] -> []
   | x::l ->
@@ -389,6 +403,9 @@ let rec list_skipn n l = match n,l with
   | _, [] -> failwith "list_fromn"
   | n, _::l -> list_skipn (pred n) l
 
+let rec list_addn n x l = 
+  if n = 0 then l else x :: (list_addn (pred n) x l)
+
 let list_prefix_of prefl l = 
   let rec prefrec = function
     | (h1::t1, h2::t2) -> h1 = h2 && prefrec (t1,t2)
@@ -410,6 +427,7 @@ let list_drop_prefix p l =
       | None -> l
 
 let list_map_append f l = List.flatten (List.map f l)
+let list_join_map = list_map_append   (* Alias *)
 
 let list_map_append2 f l1 l2 = List.flatten (List.map2 f l1 l2)
 
@@ -420,8 +438,6 @@ let list_share_tails l1 l2 =
   in 
   shr_rev [] (List.rev l1, List.rev l2)
 
-let list_join_map f l = List.flatten (List.map f l)
-
 let rec list_fold_map f e = function
   |  []  -> (e,[])
   |  h::t ->
@@ -445,13 +461,22 @@ let list_fold_map' f l e =
 
 let list_map_assoc f = List.map (fun (x,a) -> (x,f a))
 
+(* A generic cartesian product: for any operator (**), 
+   [list_cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]], 
+   and so on if there are more elements in the lists. *)
+
+let rec list_cartesian op l1 l2 = 
+  list_map_append (fun x -> List.map (op x) l2) l1
+
+(* [list_cartesians] is an n-ary cartesian product: it iterates 
+   [list_cartesian] over a list of lists.  *)
+
+let list_cartesians op init ll = 
+  List.fold_right (list_cartesian op) ll [init]
+
 (* list_combinations [[a;b];[c;d]] gives [[a;c];[a;d];[b;c];[b;d]] *)
 
-let rec list_combinations = function 
-  | [] -> [[]]
-  | l::ll -> 
-      let res = list_combinations ll in 
-      list_map_append (fun x -> List.map (fun l -> x::l) res) l
+let list_combinations l = list_cartesians (fun x l -> x::l) [] l
 
 (* Arrays *)
 
diff --git a/lib/util.mli b/lib/util.mli
index c315ecd0a..986c8e31a 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -92,7 +92,6 @@ val list_assign : 'a list -> int -> 'a -> 'a list
 val list_distinct : 'a list -> bool
 val list_duplicates : 'a list -> 'a list
 val list_filter2 : ('a -> 'b -> bool) -> 'a list * 'b list -> 'a list * 'b list
-
 (* [list_smartmap f [a1...an] = List.map f [a1...an]] but if for all i
    [ f ai == ai], then [list_smartmap f l==l] *)
 val list_smartmap : ('a -> 'a) -> 'a list -> 'a list
@@ -102,9 +101,12 @@ val list_map2_i :
   (int -> 'a -> 'b -> 'c) -> int -> 'a list -> 'b list -> 'c list
 val list_map3 :
   ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
+(* [list_index] returns the 1st index of an element in a list (counting from 1) *)
 val list_index : 'a -> 'a list -> int
 (* [list_unique_index x l] returns [Not_found] if [x] doesn't occur exactly once *)
 val list_unique_index : 'a -> 'a list -> int 
+(* [list_index0] behaves as [list_index] except that it starts counting at 0 *)
+val list_index0 : 'a -> 'a list -> int
 val list_iter_i :  (int -> 'a -> unit) -> 'a list -> unit
 val list_fold_left_i :  (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
 val list_fold_right_and_left :
@@ -118,6 +120,8 @@ val list_sep_last : 'a list -> 'a * 'a list
 val list_try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b
 val list_try_find : ('a -> 'b) -> 'a list -> 'b
 val list_uniquize : 'a list -> 'a list
+(* merges two sorted lists and preserves the uniqueness property: *)
+val list_merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
 val list_subset : 'a list -> 'a list -> bool
 val list_splitby : ('a -> bool) -> 'a list -> 'a list * 'a list
 val list_split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
@@ -125,20 +129,28 @@ val list_firstn : int -> 'a list -> 'a list
 val list_last : 'a list -> 'a
 val list_lastn : int -> 'a list -> 'a list
 val list_skipn : int -> 'a list -> 'a list 
+val list_addn : int -> 'a -> 'a list -> 'a list
 val list_prefix_of : 'a list -> 'a list -> bool
 val list_drop_prefix : 'a list -> 'a list -> 'a list
 (* [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *)
 val list_map_append : ('a -> 'b list) -> 'a list -> 'b list
+val list_join_map : ('a -> 'b list) -> 'a list -> 'b list
 (* raises [Invalid_argument] if the two lists don't have the same length *)
 val list_map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
 val list_share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list
-val list_join_map : ('a -> 'b list) -> 'a list -> 'b list
 (* [list_fold_map f e_0 [l_1...l_n] = e_n,[k_1...k_n]]
    where [(e_i,k_i)=f e_{i-1} l_i] *)
 val list_fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
 val list_fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
 val list_map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
-(* list_combinations [[a;b];[c;d]] gives [[a;c];[a;d];[b;c];[b;d]] *)
+(* A generic cartesian product: for any operator (**), 
+   [list_cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]], 
+   and so on if there are more elements in the lists. *)
+val list_cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
+(* [list_cartesians] is an n-ary cartesian product: it iterates 
+   [list_cartesian] over a list of lists.  *)
+val list_cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list
+(* list_combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *)
 val list_combinations : 'a list list -> 'a list list
 
 
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 11c9ff48a..ecb2e132a 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -44,7 +44,7 @@ let rec index_and_rec_order_of_annot loc bl ann =
     | [_], (None, r) -> Some 0, r
     | lids, (Some x, ro) ->
         let ids = List.map snd lids in
-        (try Some (list_index (snd x) ids - 1), ro
+        (try Some (list_index0 (snd x) ids), ro
         with Not_found ->
           user_err_loc(fst x,"index_of_annot", Pp.str"no such fix variable"))
     | _, (None, r) -> None, r
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f7078aa00..c128ff7af 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -253,7 +253,7 @@ GEXTEND Gram
           let ni =
             match fst annot with
                 Some id ->
-                  (try Some (list_index (Name id) names - 1)
+                  (try Some (list_index0 (Name id) names)
                    with Not_found ->  Util.user_err_loc
                      (loc,"Fixpoint",
                       Pp.str "No argument named " ++ Nameops.pr_id id))
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index aceba6e25..b62bf5820 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -247,9 +247,6 @@ module SearchProblem = struct
 	with e when Logic.catchable_exception e ->
 	  filter_tactics (glls,v) tacl
 
-  let rec list_addn n x l = 
-    if n = 0 then l else x :: (list_addn (pred n) x l)
-
   (* Ordering of states is lexicographic on depth (greatest first) then
      number of remaining goals. *)
   let compare s s' =