diff options
| author | Hugo Herbelin | 2015-05-01 11:33:59 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-05-01 11:36:08 +0200 |
| commit | f19d0c7baf91fb410de77baed391b0a16db9c4e2 (patch) | |
| tree | 68fcfd2fb2ea36c7c1e7293833a5c4a941b456ae /test-suite/bugs/closed | |
| parent | 857e82b2ca0d164242070599b66138cc431509c9 (diff) | |
Fixing computation of implicit arguments by position in fixpoints (#4217).
Diffstat (limited to 'test-suite/bugs/closed')
| -rw-r--r-- | test-suite/bugs/closed/4217.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4217.v b/test-suite/bugs/closed/4217.v new file mode 100644 index 0000000000..19973f30a7 --- /dev/null +++ b/test-suite/bugs/closed/4217.v @@ -0,0 +1,6 @@ +(* Checking correct index of implicit by pos in fixpoints *) + +Fixpoint ith_default + {default_A : nat} + {As : list nat} + {struct As} : Set. |