diff options
| author | Hugo Herbelin | 2014-11-07 19:46:19 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-11-07 20:10:17 +0100 |
| commit | b3eb49d5e32ea8456d4f840b22639e5f5a9a354c (patch) | |
| tree | d2e1de457a27f558cfa37cc3df1184f830f83eaa | |
| parent | 044a44f1a877764b13418b8865adff76cf0c6f93 (diff) | |
Test for #3542 fixed some time ago.
| -rw-r--r-- | test-suite/bugs/closed/3542.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3542.v b/test-suite/bugs/closed/3542.v new file mode 100644 index 0000000000..b6837a0c33 --- /dev/null +++ b/test-suite/bugs/closed/3542.v @@ -0,0 +1,6 @@ +Section foo. + Context {A:Type} {B : A -> Type}. + Context (f : forall x, B x). + Goal True. + pose (r := fun k => existT (fun g => forall x, f x = g x) + (fun x => projT1 (k x)) (fun x => projT2 (k x))). |