diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-28 21:30:59 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-17 18:47:10 +0200 |
| commit | d41eaff0b2c6f2ff10ef851864abfa3366862d22 (patch) | |
| tree | 7263955a94456d9cefe395ea719b37d97409d60a /engine/universes.ml | |
| parent | 302adae094bbf76d8c951c557c85acb12a97aedc (diff) | |
Make Universes.refresh_constraints internal to UState
Diffstat (limited to 'engine/universes.ml')
| -rw-r--r-- | engine/universes.ml | 18 |
1 files changed, 0 insertions, 18 deletions
diff --git a/engine/universes.ml b/engine/universes.ml index 009328571..e3b661770 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -384,24 +384,6 @@ let normalize_context_set g ctx us algs weak = (* let normalize_conkey = CProfile.declare_profile "normalize_context_set" *) (* let normalize_context_set a b c = CProfile.profile3 normalize_conkey normalize_context_set a b c *) -let is_trivial_leq (l,d,r) = - Univ.Level.is_prop l && (d == Univ.Le || (d == Univ.Lt && Univ.Level.is_set r)) - -(* Prop < i <-> Set+1 <= i <-> Set < i *) -let translate_cstr (l,d,r as cstr) = - if Level.equal Level.prop l && d == Univ.Lt && not (Level.equal Level.set r) then - (Level.set, d, r) - else cstr - -let refresh_constraints univs (ctx, cstrs) = - let cstrs', univs' = - Univ.Constraint.fold (fun c (cstrs', univs as acc) -> - let c = translate_cstr c in - if is_trivial_leq c then acc - else (Univ.Constraint.add c cstrs', UGraph.enforce_constraint c univs)) - cstrs (Univ.Constraint.empty, univs) - in ((ctx, cstrs'), univs') - (** Deprecated *) (** UnivNames *) |