From 92616b9f660eaa2640964ca1925b05d37af70c8c Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Sat, 15 Sep 2012 00:39:54 +0000
Subject: Some documentation and cleaning of CList and Util interfaces.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15805 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/funind/glob_term_to_relation.ml | 2 +-
 plugins/funind/invfun.ml                | 3 ++-
 2 files changed, 3 insertions(+), 2 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 490d52555c..b820489f53 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1238,7 +1238,7 @@ let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * b
   let l = ref [] in
   let _ =
     try
-      List.iter_i
+      List.iteri
 	(fun i ((n,nt,is_defined) as param) ->
 	   if Array.for_all
 	     (fun l ->
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d8255e8342..bbc9ff93b3 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -122,10 +122,11 @@ let generate_type g_to_f f graph i =
       | _ -> let j = !i in incr i;mkRel (nb_args - j  + 1)
   in
   (*i We need to name the vars [res] and [fv] i*)
+  let filter = function (Name id,_,_) -> Some id | (Anonymous,_,_) -> None in
   let res_id =
     Namegen.next_ident_away_in_goal
       (id_of_string "res")
-      (map_succeed (function (Name id,_,_) -> id | (Anonymous,_,_) -> failwith "") fun_ctxt)
+      (List.map_filter filter fun_ctxt)
   in
   let fv_id =
     Namegen.next_ident_away_in_goal
-- 
cgit v1.2.3