diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-03-16 18:18:54 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-03-16 18:18:54 +0100 |
| commit | 4849c8eb1b7a386d2abcbc80c40de34b0a69b8ea (patch) | |
| tree | 75a05a4596ba8ea13b67dd93a9ce69cbc2518d56 /test-suite/bugs/4624.v | |
| parent | bfce815bd1fa2c603141661b209a864c67ae1dbf (diff) | |
Test file for #4624, fixed by Matthieu's bfce815bd1.
Diffstat (limited to 'test-suite/bugs/4624.v')
| -rw-r--r-- | test-suite/bugs/4624.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/bugs/4624.v b/test-suite/bugs/4624.v new file mode 100644 index 000000000..a737afcda --- /dev/null +++ b/test-suite/bugs/4624.v @@ -0,0 +1,7 @@ +Record foo := mkfoo { type : Type }. + +Canonical Structure fooA (T : Type) := mkfoo (T -> T). + +Definition id (t : foo) (x : type t) := x. + +Definition bar := id _ ((fun x : nat => x) : _).
\ No newline at end of file |