diff options
author | 2018-06-25 18:26:55 +0200 | |
---|---|---|
committer | 2018-06-25 18:26:55 +0200 | |
commit | a1fc621b943dbf904705dc88ed27c26daf4c5e72 (patch) | |
tree | 2649ab1a1480b17b74c7207113d5ae8783f2ee42 /kernel/univ.ml | |
parent | 24279abf43cfbd65e2fc29f171eb8705fdf61a3e (diff) | |
parent | 1311a2bf08ac1deb16f0b3064bc1164d75858a97 (diff) |
Merge PR #7798: Remove hack skipping comparison of algebraic universes in subtyping.
Diffstat (limited to 'kernel/univ.ml')
-rw-r--r-- | kernel/univ.ml | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 9782312ca..311477dac 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -666,7 +666,7 @@ let constraint_add_leq v u c = else (* j >= 1 *) (* m = n + k, u <= v+k *) if Level.equal x y then c (* u <= u+k, trivial *) else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *) - else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints.") + else Constraint.add (x,Le,y) c (* u <= v implies u <= v+k *) let check_univ_leq_one u v = Universe.exists (Expr.leq u) v @@ -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 |