diff options
| author | Matthieu Sozeau | 2014-04-07 17:29:26 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:59 +0200 |
| commit | 2d6de8b102ea3cd05c5d193190faf787ccb84baa (patch) | |
| tree | 876350b54e58c77b0bb265afa65a04acd0536872 /library | |
| parent | d081f9390206c510d9837e2ecd3fa0a0d4ef0b8c (diff) | |
Fix restrict_universe_context removing some universes that do appear in the term.
Diffstat (limited to 'library')
| -rw-r--r-- | library/universes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/universes.ml b/library/universes.ml index 2ed477d67b..7d1908d1f5 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -673,7 +673,7 @@ let restrict_universe_context (univs,csts) s = if LSet.mem l diff && LSet.mem r diff then (univs, csts) else (LSet.add l (LSet.add r univs), Constraint.add c csts)) csts (LSet.empty, Constraint.empty) - in (LSet.inter univs univscstrs, csts) + in (LSet.union s (LSet.inter univs univscstrs), csts) let simplify_universe_context (univs,csts) = let uf = UF.create () in |