diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-06-19 19:03:52 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-06-19 19:23:37 +0200 |
| commit | 676c93e4bee82a4e6528fbf42be28efe473b1871 (patch) | |
| tree | a151448870c35878a384df518a2655313c87d6cc /kernel | |
| parent | 6715e6801c1d285a12eeca55dd8b831d7efb8c0d (diff) | |
Fix Univ.enforce_leq dropped constraints when algebraic on the right
There's probably a proof of false using subtyping if someone wants to
look.
NB: the checker doesn't handle algebraics on the right.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/univ.ml | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 9782312ca..2b4a1c50c 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -674,12 +674,7 @@ let check_univ_leq u v = Universe.for_all (fun u -> check_univ_leq_one u v) u let enforce_leq u v c = - let rec aux acc v = - match v with - | v :: l -> - aux (List.fold_right (fun u -> constraint_add_leq u v) u c) l - | [] -> acc - in aux c v + List.fold_left (fun c v -> (List.fold_left (fun c u -> constraint_add_leq u v c) c u)) c v let enforce_leq u v c = if check_univ_leq u v then c |