Refl_omega: replaced some generic = on constr by eq_constr

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

1 files changed, 9 insertions, 0 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