Mercurial > cpdt > repo
diff src/DepList.v @ 568:81d63d9c1cc5
Port to Coq 8.9.0
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sun, 20 Jan 2019 15:16:29 -0500 |
| parents | ed829eaa91b2 |
| children | 0ce9829efa3b |
line wrap: on
line diff
--- a/src/DepList.v Sun Jan 20 15:00:32 2019 -0500 +++ b/src/DepList.v Sun Jan 20 15:16:29 2019 -0500 @@ -107,8 +107,8 @@ End fold. End ilist. -Implicit Arguments INil [A]. -Implicit Arguments First [n]. +Arguments INil [A]. +Arguments First [n]. Section imap. Variables A B : Type. @@ -197,12 +197,12 @@ Qed. End hlist. -Implicit Arguments HNil [A B]. -Implicit Arguments HCons [A B x ls]. -Implicit Arguments hmake [A B]. +Arguments HNil [A B]. +Arguments HCons [A B x ls]. +Arguments hmake [A B]. -Implicit Arguments HFirst [A elm ls]. -Implicit Arguments HNext [A elm x ls]. +Arguments HFirst [A elm 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. -Implicit Arguments hmap [A B1 B2 ls]. +Arguments hmap [A B1 B2] f [ls].