diff options
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 76bd88cc0..f2f922fd5 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -566,7 +566,8 @@ let force_eqs c = Constraints.fold (fun c acc -> let c' = match c with - | ULub (l, r) -> UEq (Univ.Universe.make l,Univ.Universe.make r) + (* Should we be forcing weak constraints? *) + | ULub (l, r) | UWeak (l, r) -> UEq (Univ.Universe.make l,Univ.Universe.make r) | ULe _ | UEq _ -> c in Constraints.add c' acc) |