Mercurial > cpdt > repo
diff src/DepList.v @ 574:1dc1d41620b6
Builds with Coq 8.15.2
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sun, 31 Jul 2022 14:48:22 -0400 |
parents | 0ce9829efa3b |
children |
line wrap: on
line diff
--- a/src/DepList.v Sun Feb 02 10:51:18 2020 -0500 +++ b/src/DepList.v Sun Jul 31 14:48:22 2022 -0400 @@ -107,8 +107,8 @@ End fold. End ilist. -Arguments INil [A]. -Arguments First [n]. +Arguments INil {A}. +Arguments First {n}. Section imap. Variables A B : Type. @@ -197,11 +197,11 @@ Qed. End hlist. -Arguments HNil [A B]. +Arguments HNil {A B}. Arguments HCons [A B x ls] _ _. Arguments hmake [A B] f ls. -Arguments HFirst [A elm ls]. +Arguments HFirst {A elm ls}. Arguments HNext [A elm x ls] _. Infix ":::" := HCons (right associativity, at level 60).