Commit 11d58fc1 authored by POTTIER Francois's avatar POTTIER Francois

Fix `Option.equal`.

parent 55cf9dda
......@@ -9,13 +9,16 @@ module Make (X : sig type t end) = struct
None
let equal (o1 : property) (o2 : property) =
(* It is permitted to assume that [o1 <= o2] holds. This implies
that, when [o1] is [Some x1] and [o2] is [Some x2], we may return
[true] without actually comparing [x1] and [x2]. *)
(* It is permitted to assume that [o1 <= o2] holds. This implies that
when [o1] is [Some x1] and [o2] is [Some x2] we may return [true]
without actually comparing [x1] and [x2]. *)
match o1, o2 with
| Some _, None ->
(* Because [o1 <= o2] holds, this cannot happen. *)
assert false
| None, Some _ ->
false
| None, _
| None, None
| Some _, Some _ ->
true
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment