diff options
| author | Maxime Dénès | 2016-12-04 12:03:18 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2016-12-04 12:03:18 +0100 |
| commit | f653036a73f008168809d3f50041382fe3ee52a1 (patch) | |
| tree | d9c9545e7515c3701434571f84b0aef74bf50158 /engine/evd.ml | |
| parent | 36df551d64a01e5f1fa7fe2ffdcbf1cb68b268cd (diff) | |
| parent | b8c0f76e507dc0c5dbae3ea7a89d78f16b4a7acb (diff) | |
Merge remote-tracking branch 'github/pr/366' into v8.6
Was PR#366: Univs: fix bug 5208
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index aa91fc5222..a6b6f742b7 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -854,6 +854,13 @@ let is_eq_sort s1 s2 = if Univ.Universe.equal u1 u2 then None else Some (u1, u2) +(* Precondition: l is not defined in the substitution *) +let universe_rigidity evd l = + let uctx = evd.universes in + if Univ.LSet.mem l (Univ.ContextSet.levels (UState.context_set uctx)) then + UnivFlexible (Univ.LSet.mem l (UState.algebraics uctx)) + else UnivRigid + let normalize_universe evd = let vars = ref (UState.subst evd.universes) in let normalize = Universes.normalize_universe_opt_subst vars in |