diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/README.md | 2 | ||||
| -rw-r--r-- | test-suite/success/uniform_inductive_parameters.v | 18 |
2 files changed, 15 insertions, 5 deletions
diff --git a/test-suite/README.md b/test-suite/README.md index a2d5905710..96926f70b9 100644 --- a/test-suite/README.md +++ b/test-suite/README.md @@ -67,7 +67,7 @@ See [`test-suite/Makefile`](Makefile) for more information. ## Adding a test Regression tests for closed bugs should be added to -[`bugs/closed`](bugs/closed), as `1234.v` where `1234` is the bug number. +[`bugs/closed`](bugs/closed), as `bug_1234.v` where `1234` is the bug number. Files in this directory are tested for successful compilation. When you fix a bug, you should usually add a regression test here as well. diff --git a/test-suite/success/uniform_inductive_parameters.v b/test-suite/success/uniform_inductive_parameters.v index 42236a5313..651247937d 100644 --- a/test-suite/success/uniform_inductive_parameters.v +++ b/test-suite/success/uniform_inductive_parameters.v @@ -1,13 +1,23 @@ +Module Att. + #[uniform] Inductive list (A : Type) := + | nil : list + | cons : A -> list -> list. + Check (list : Type -> Type). + Check (cons : forall A, A -> list A -> list A). +End Att. + Set Uniform Inductive Parameters. Inductive list (A : Type) := - | nil : list - | cons : A -> list -> list. +| nil : list +| cons : A -> list -> list. Check (list : Type -> Type). Check (cons : forall A, A -> list A -> list A). Inductive list2 (A : Type) (A' := prod A A) := - | nil2 : list2 - | cons2 : A' -> list2 -> list2. +| nil2 : list2 +| cons2 : A' -> list2 -> list2. Check (list2 : Type -> Type). Check (cons2 : forall A (A' := prod A A), A' -> list2 A -> list2 A). + +#[nonuniform] Inductive bla (n:nat) := c (_ : bla (S n)). |