diff options
| author | Matthieu Sozeau | 2014-04-02 17:24:30 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:58 +0200 |
| commit | b17c1e128fad2e84ebe4e4742b47bd67d88c56d6 (patch) | |
| tree | bac92e1b2ffee60a4a33618c29d2a61b49bdb64a | |
| parent | a2fce6d14d00a437466a1f7e3b53a77229f87980 (diff) | |
Fix restrict_universe_context to not remove useful constraints.
| -rw-r--r-- | library/universes.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/library/universes.ml b/library/universes.ml index 5996d7a80f..2ed477d67b 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -664,16 +664,16 @@ let shrink_universe_context (univs,csts) s = csts (univs',Constraint.empty) let restrict_universe_context (univs,csts) s = - let univs' = LSet.inter univs s in (* Universes that are not necessary to typecheck the term. E.g. univs introduced by tactics and not used in the proof term. *) let diff = LSet.diff univs s in - let csts' = - Constraint.fold (fun (l,d,r as c) csts -> - if LSet.mem l diff || LSet.mem r diff then csts - else Constraint.add c csts) - csts Constraint.empty - in (univs', csts') + let (univscstrs, csts) = + Constraint.fold + (fun (l,d,r as c) (univs, csts) -> + 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) let simplify_universe_context (univs,csts) = let uf = UF.create () in |