diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-13 12:19:47 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-13 12:22:34 +0100 |
| commit | 50c948480647af3c5aaea5f80fa9f3341471f2b0 (patch) | |
| tree | 26f18a3c560197dede4932f02b4ac4d8a4acc701 /test-suite/success/Inductive.v | |
| parent | d2fb531761e1f4fa02d0c7e7b5b51febe48e357e (diff) | |
Fixing an anomaly in the presence of "let-in" in the type of a record.
Was raised by Jason on Gitter.
Diffstat (limited to 'test-suite/success/Inductive.v')
| -rw-r--r-- | test-suite/success/Inductive.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 893d75b77..5b1482fd5 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -200,3 +200,9 @@ Module NonRecLetIn. (fun n b c => f_equal (Rec n) eq_refl) 0 (Rec 0 (Base 1)). End NonRecLetIn. + +(* Test treatment of let-in in the definition of Records *) +(* Should fail with "Sort expected" *) + +Fail Inductive foo (T : Type) : let T := Type in T := + { r : forall x : T, x = x }. |