diff options
| author | Hugo Herbelin | 2017-08-24 15:18:23 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-02-20 10:03:06 +0100 |
| commit | 5806b0476a1ac9b903503641cc3e2997d3e8d960 (patch) | |
| tree | fc77bdb02dec76f18af12c045620eca52f8b03e6 /clib/cList.mli | |
| parent | e4d93d1cef27d3a8c1e36139fc1e118730406f67 (diff) | |
When printing a notation with "match", more flexibility in matching equations.
We reason up to order, and accept to match a final catch-all clauses
with any other clause.
This allows for instance to parse and print a notation of the form
"if t is S n then p else q".
Diffstat (limited to 'clib/cList.mli')
| -rw-r--r-- | clib/cList.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/clib/cList.mli b/clib/cList.mli index cb062d5c8f..b3ee28548c 100644 --- a/clib/cList.mli +++ b/clib/cList.mli @@ -127,7 +127,7 @@ sig exception otherwise; sets should have the same size; raise the given exception if no pairing of the two sets is found;; complexity in O(n^2) *) - val fold_left2_set : exn -> ('a -> 'b -> 'c -> 'a) -> 'a -> 'b list -> 'c list -> 'a + val fold_left2_set : exn -> ('a -> 'b -> 'c -> 'b list -> 'c list -> 'a) -> 'a -> 'b list -> 'c list -> 'a val for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool val except : 'a eq -> 'a -> 'a list -> 'a list |