3 files changed, 12 insertions, 1 deletions
diff --git a/lib/util.ml b/lib/util.ml
index 94b1d37c2..e9f87acb5 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -507,6 +507,15 @@ let rec list_smartfilter f l = match l with
 	  else h :: tl'
 	else tl'
 	  
+let list_index_f 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 list_index0_f f x l = list_index_f f x l - 1
+
 let list_index x =
   let rec index_x n = function
     | y::l -> if x = y then n else index_x (succ n) l
diff --git a/lib/util.mli b/lib/util.mli
index 8a26c9890..7b8f9d31d 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -154,12 +154,14 @@ val list_smartfilter : ('a -> bool) -> 'a list -> 'a list
 
 (** [list_index] returns the 1st index of an element in a list (counting from 1) *)
 val list_index : 'a -> 'a list -> int
+val list_index_f : ('a -> 'a -> bool) -> '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_index0_f : ('a -> 'a -> bool) -> 'a -> 'a list -> int
 val list_iter3 : ('a -> 'b -> 'c -> unit) -> 'a list -> 'b list -> 'c list -> unit
 val list_iter_i :  (int -> 'a -> unit) -> 'a list -> unit
 val list_fold_right_i :  (int -> 'a -> 'b -> 'b) -> int -> 'a list -> 'b -> 'b
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 570bb1877..d27b52259 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -219,7 +219,7 @@ let unintern_omega env id =
    calcul des variables utiles. *)
 
 let add_reified_atom t env =
-  try list_index0 t env.terms
+  try list_index0_f Term.eq_constr t env.terms
   with Not_found ->
     let i = List.length env.terms in
     env.terms <- env.terms @ [t]; i