diff options
Diffstat (limited to 'library/universes.ml')
| -rw-r--r-- | library/universes.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/library/universes.ml b/library/universes.ml index 138a248f0..5996d7a80 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -594,13 +594,12 @@ let normalize_context_set ctx us algs = let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in (* Add equalities for globals which can't be merged anymore. *) let cstrs = LSet.fold (fun g cst -> - Constraint.add (canon, Univ.Eq, g) cst) global cstrs + Constraint.add (canon, Univ.Eq, g) cst) (LSet.union global rigid) + cstrs in - (** Should this really happen? *) - let subst' = LSet.fold (fun f -> LMap.add f canon) - (LSet.union rigid flexible) LMap.empty + let subst = LSet.fold (fun f -> LMap.add f canon) + flexible subst in - let subst = LMap.union subst' subst in (subst, cstrs)) (LMap.empty, Constraint.empty) partition in |