aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/util.mli
diff options
context:
space:
mode:
authorGravatar aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-12-06 14:24:53 +0000
committerGravatar aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-12-06 14:24:53 +0000
commit3e3fa18a066feae44c10fc6e072059f4e9914656 (patch)
tree6ff163fd7561bf8c0823c7508acf83b350d4511d /lib/util.mli
parentfb75bd254df2eadfc8abd45a646dfe9b1c4a53b6 (diff)
Commit intermédiaire express de réparation de coqide.ml, que j'avais
tout cassé hier sans m'en rendre compte (le soucis de travailler sur un ordinateur où j'ai pas installé lablgtk2). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10347 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/util.mli')
-rw-r--r--lib/util.mli3
1 files changed, 0 insertions, 3 deletions
diff --git a/lib/util.mli b/lib/util.mli
index 0282f45f5..71262bb4c 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -223,10 +223,7 @@ val intmap_inv : 'a Intmap.t -> 'a -> int list
val interval : int -> int -> int list
-val in_some : 'a -> 'a option
val option_cons : 'a option -> 'a list -> 'a list
-val option_fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option ->
- 'c option -> 'a
val option_compare : ('a -> 'b -> bool) -> 'a option -> 'b option -> bool
val filter_some : 'a option list -> 'a list