diff options
| author | Gaëtan Gilbert | 2019-02-07 12:29:39 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-12 17:16:39 +0100 |
| commit | 7104904f9f6e1a5e1b1590bd898ae20cb7178daf (patch) | |
| tree | 7096fac4343b585e9fd168ce753d53ae8f0cdd1e | |
| parent | 75269e1b3fb98c8095b7f50e8ade2af87eb4061f (diff) | |
Fix failing coqtops universe-polymorphism.rst
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 04aedd0cf6..6b10b7c0b3 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -223,7 +223,7 @@ The following is an example of a record with non-trivial subtyping relation: E[Γ] ⊢ \mathsf{packType}@\{i\} =_{βδιζη} \mathsf{packType}@\{j\}~\mbox{ whenever }~i ≤ j -Cumulative inductive types, coninductive types, variants and records +Cumulative inductive types, coinductive types, variants and records only make sense when they are universe polymorphic. Therefore, an error is issued whenever the user uses the :g:`Cumulative` or :g:`NonCumulative` prefix in a monomorphic context. @@ -236,11 +236,11 @@ Consider the following examples. .. coqtop:: all reset - Monomorphic Cumulative Inductive Unit := unit. + Fail Monomorphic Cumulative Inductive Unit := unit. .. coqtop:: all reset - Monomorphic NonCumulative Inductive Unit := unit. + Fail Monomorphic NonCumulative Inductive Unit := unit. .. coqtop:: all reset |