diff options
| author | Matthieu Sozeau | 2019-03-26 18:53:32 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-03-26 18:53:32 +0100 |
| commit | 2ac275c0f3e65a402951de86a61c77dd0e0782f8 (patch) | |
| tree | 797d2176e120935f1acb9342f1a5751f2c38618c /test-suite | |
| parent | 0ff2e4b9f845ff280ee7adb865f837bc6040efbf (diff) | |
| parent | b4561c5047eb2383c2b718fd1cf9da8076497511 (diff) | |
Merge PR #9690: Fix 9663 (Miller pattern unification fails on evars)
Ack-by: ggonthier
Reviewed-by: mattam82
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_9663.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_9663.v b/test-suite/bugs/closed/bug_9663.v new file mode 100644 index 0000000000..b5fa601278 --- /dev/null +++ b/test-suite/bugs/closed/bug_9663.v @@ -0,0 +1,2 @@ +Definition id_depfn S T (f : forall x : S, T x) := f. +Definition idn : nat -> nat := @id_depfn _ _ (fun x => x). |