diff options
| author | herbelin | 2006-03-29 21:06:33 +0000 |
|---|---|---|
| committer | herbelin | 2006-03-29 21:06:33 +0000 |
| commit | 6f3b7eb486426ef8104b9b958088315342845795 (patch) | |
| tree | 7a5553ae26b1aac0ed72f182dae7ae2642847ea8 /library | |
| parent | f4c41760e935836315cb26f165d2c720cfbf89cb (diff) | |
Ajout array_fold_map', list_fold_map' et list_remove_first
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8672 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
| -rw-r--r-- | library/impargs.ml | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index fe0e2cca47..404e06f991 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -385,11 +385,6 @@ let implicits_of_global r = (* Declare manual implicits *) -let rec list_remove a = function - | b::l when a = b -> l - | b::l -> b::list_remove a l - | [] -> raise Not_found - let set_implicit id imp = Some (id,match imp with None -> Manual | Some imp -> imp) @@ -403,9 +398,9 @@ let declare_manual_implicits r l = let rec merge k l = function | (Name id,imp)::imps -> let l',imp = - try list_remove (ExplByPos k) l, set_implicit id imp + try list_remove_first (ExplByPos k) l, set_implicit id imp with Not_found -> - try list_remove (ExplByName id) l, set_implicit id imp + try list_remove_first (ExplByName id) l, set_implicit id imp with Not_found -> l, None in imp :: merge (k+1) l' imps |