Stefan pushed to branch master at Stefan / Typer

Commits: ef053aac by Stefan Monnier at 2017-07-19T15:36:46-04:00 Force TypeLevel parameters to come first

- - - - -

2 changed files:

- doc/manual.texi - src/opslexp.ml

Changes:

===================================== doc/manual.texi ===================================== --- a/doc/manual.texi +++ b/doc/manual.texi @@ -210,7 +210,6 @@ A = { TypeLevel : SortL, } R = { (SortL, Type l, Sortω), ∀ l : TypeLevel (SortL, Sortω, Sortω), - (Type l, Sortω, Sortω), ∀ l : TypeLevel (Type l₁, Type l₂, Type (TypeLevel.∪ l₁ l₂)) ∀ l₁,l₂ : TypeLevel } @end example

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -332,8 +332,11 @@ let sort_compose meta_ctx ctx l s1 s2 = match s1, s2 with | (Stype l1, Stype l2) -> Stype (mkSLlub meta_ctx ctx l1 l2) | ( (StypeLevel, Stype _) - | (StypeLevel, StypeOmega) - | (Stype _, StypeOmega)) + | (StypeLevel, StypeOmega) + (* This is probably safe, but I don't think it adds much power nor + * flexibility, so let's not bother for now: it's easier to add it later + * than to remove it later. + * | (Stype _, StypeOmega) *)) -> StypeOmega | _,_ -> (U.msg_error "TC" l "Mismatch sorts for arg and result";

View it on GitLab: https://gitlab.com/monnier/typer/commit/ef053aac6a6b2ed613342213c5ed8ad1da28...

--- View it on GitLab: https://gitlab.com/monnier/typer/commit/ef053aac6a6b2ed613342213c5ed8ad1da28... You're receiving this email because of your account on gitlab.com.