diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-06-23 15:40:16 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-06-26 16:26:30 +0200 |
| commit | d9ac4c22a3a6543959d413120304e356d625c0f9 (patch) | |
| tree | 55379f83d5a3a26a3ebae76d2efb80e2cc09ee9e /pretyping/evd.ml | |
| parent | 3e0aa07cfb1d552e11b37aaf5f0224bfb5b47523 (diff) | |
Fix bug #4254 with the help of J.H. Jourdan
1) We now _assign_ the smallest possible arities to mutual inductive types
and eventually add leq constraints on the user given arities. Remove
useless limitation on instantiating algebraic universe variables with
their least upper bound if they have upper constraints as well.
2) Do not remove non-recursive variables when computing minimal levels of inductives.
3) Avoid modifying user-given arities if not necessary to compute the
minimal level of an inductive.
4) We correctly solve the recursive equations taking into account the
user-declared level.
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 60b1da704..168a10df9 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -351,10 +351,7 @@ let evar_universe_context_of ctx = { empty_evar_universe_context with uctx_local let evar_universe_context_subst ctx = ctx.uctx_univ_variables let instantiate_variable l b v = - (* let b = Univ.subst_large_constraint (Univ.Universe.make l) Univ.type0m_univ b in *) - (* if Univ.univ_depends (Univ.Universe.make l) b then *) - (* error ("Occur-check in universe variable instantiation") *) - (* else *) v := Univ.LMap.add l (Some b) !v + v := Univ.LMap.add l (Some b) !v exception UniversesDiffer @@ -420,7 +417,16 @@ let process_universe_constraints univs vars alg cstrs = raise UniversesDiffer in Univ.enforce_eq_level l' r' local - | _, _ (* One of the two is algebraic or global *) -> + | Inr (l, loc, alg), Inl r + | Inl r, Inr (l, loc, alg) -> + let inst = Univ.univ_level_rem l r r in + if alg then (instantiate_variable l inst vars; local) + else + let lu = Univ.Universe.make l in + if Univ.univ_level_mem l r then + Univ.enforce_leq inst lu local + else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None)) + | _, _ (* One of the two is algebraic or global *) -> if Univ.check_eq univs l r then local else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None)) in |