diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2018-06-25 18:26:55 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2018-06-25 18:26:55 +0200 |
| commit | a1fc621b943dbf904705dc88ed27c26daf4c5e72 (patch) | |
| tree | 2649ab1a1480b17b74c7207113d5ae8783f2ee42 /vernac | |
| parent | 24279abf43cfbd65e2fc29f171eb8705fdf61a3e (diff) | |
| parent | 1311a2bf08ac1deb16f0b3064bc1164d75858a97 (diff) | |
Merge PR #7798: Remove hack skipping comparison of algebraic universes in subtyping.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 5d671ef52..534e58f9c 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -871,9 +871,6 @@ let explain_not_match_error = function pr_enum (function Name id -> Id.print id | _ -> str "_") nal | NotEqualInductiveAliases -> str "Aliases to inductive types do not match" - | NoTypeConstraintExpected -> - strbrk "a definition whose type is constrained can only be subtype " ++ - strbrk "of a definition whose type is itself constrained" | CumulativeStatusExpected b -> let status b = if b then str"cumulative" else str"non-cumulative" in str "a " ++ status b ++ str" declaration was expected, but a " ++ |