diff options
| author | Hugo Herbelin | 2014-10-07 17:26:02 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-07 18:40:36 +0200 |
| commit | 38b34dfffcceab7fa7d5ba43c84e414d24cebe43 (patch) | |
| tree | c5449cf9c02c97586bf8a8edaa52d05d876d3e94 /lib/cList.mli | |
| parent | 2313bde0116a5916912bebbaca77d291f7b2760a (diff) | |
Splitting out of auto.ml a file hints.ml dedicated to hints so as to
being able to export hints without tactics, vm, etc. to come with.
Some functions moved to the new proof engine.
Diffstat (limited to 'lib/cList.mli')
| -rw-r--r-- | lib/cList.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/lib/cList.mli b/lib/cList.mli index 01ae839601..aa888679c6 100644 --- a/lib/cList.mli +++ b/lib/cList.mli @@ -119,6 +119,10 @@ sig val remove_first : ('a -> bool) -> 'a list -> 'a list (** Remove the first element satisfying a predicate, or raise [Not_found] *) + val insert : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list + (** Insert at the (first) position so that if the list is ordered wrt to the + total order given as argument, the order is preserved *) + val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool val sep_last : 'a list -> 'a * 'a list |