Mercurial > cpdt > repo
diff src/DepList.v @ 569:0ce9829efa3b
Back to working in Coq 8.4
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sun, 20 Jan 2019 15:28:23 -0500 |
| parents | 81d63d9c1cc5 |
| children | 1dc1d41620b6 |
line wrap: on
line diff
--- a/src/DepList.v Sun Jan 20 15:16:29 2019 -0500 +++ b/src/DepList.v Sun Jan 20 15:28:23 2019 -0500 @@ -198,11 +198,11 @@ End hlist. Arguments HNil [A B]. -Arguments HCons [A B x ls]. -Arguments hmake [A B]. +Arguments HCons [A B x ls] _ _. +Arguments hmake [A B] f ls. Arguments HFirst [A elm ls]. -Arguments HNext [A elm x ls]. +Arguments HNext [A elm x ls] _. Infix ":::" := HCons (right associativity, at level 60). Infix "+++" := happ (right associativity, at level 60). @@ -233,4 +233,4 @@ Qed. End hmap. -Arguments hmap [A B1 B2] f [ls]. +Arguments hmap [A B1 B2] f [ls] hl.