File tree 1 file changed +7
-2
lines changed
1 file changed +7
-2
lines changed Original file line number Diff line number Diff line change @@ -1339,6 +1339,10 @@ module Monadic = struct
1339
1339
let uniqueness m =
1340
1340
S.Negative. via_monotone Uniqueness.Obj. obj (Proj (Obj. obj, Uniqueness )) m
1341
1341
1342
+ (* The monadic fragment is inverted. Most of the inversion logic is taken care
1343
+ by [Solver_polarized], but some remain, such as the [Min_with] below which
1344
+ is inverted from [Max_with]. *)
1345
+
1342
1346
let max_with_uniqueness m =
1343
1347
S.Negative. via_monotone Obj. obj (Min_with Uniqueness )
1344
1348
(S.Negative. disallow_left m)
@@ -1368,8 +1372,9 @@ module Monadic = struct
1368
1372
match submode m0 m1 with
1369
1373
| Ok () -> Ok ()
1370
1374
| Error { left = uni0 , () ; right = uni1 , () } ->
1371
- assert (not (Uniqueness.Const. le uni0 uni1));
1372
- Error (`Uniqueness { left = uni0; right = uni1 })
1375
+ if Uniqueness.Const. le uni0 uni1
1376
+ then assert false
1377
+ else Error (`Uniqueness { left = uni0; right = uni1 })
1373
1378
1374
1379
(* override to report the offending axis *)
1375
1380
let equate = equate_from_submode submode
You can’t perform that action at this time.
0 commit comments