19 commits

Author	SHA1	Message	Date
Adam Chlipala	f3211734b9	A big pass to stop Coq from complaining about missing locality annotations	2022-03-07 13:48:40 -05:00
Adam Chlipala	d745f0802e	Ported to Coq 8.15	2022-01-29 15:13:09 -05:00
Adam Chlipala	b549b15af7	Revising for next lecture	2021-04-18 16:23:25 -04:00
Adam Chlipala	75ea3ed0b3	Chapter renumbering	2021-03-28 17:03:56 -04:00
Adam Chlipala	d3c7a85b49	More cleanup around addition of RuleInduction	2021-03-01 12:15:34 -05:00
Adam Chlipala	ca3a490119	Revising before class	2020-04-08 10:48:14 -04:00
Adam Chlipala	89f21b8533	First phase of update for Coq 8.10	2020-02-02 17:16:19 -05:00
Adam Chlipala	7c06dc3541	Proofreading DeepAndShallowEmbeddings	2018-04-22 14:07:01 -04:00
Adam Chlipala	db0f87d654	DeepAndShallowEmbeddings: comment typo fix	2017-04-24 09:28:48 -04:00
Adam Chlipala	2832696faa	Start of CompilerCorrectness: cfoldExprs_ok	2017-03-18 14:42:13 -04:00
Adam Chlipala	b27e58f11e	Bump chapter numbers in Coq code comments	2017-02-21 09:00:30 -05:00
Adam Chlipala	145bff88c6	DeepAndShallowEmbeddings: Coq 8.4 support	2016-04-11 08:13:49 -04:00
Adam Chlipala	e50cbae0c3	DeepAndShallowEmbeddings: comments	2016-04-10 19:50:20 -04:00
Adam Chlipala	7a49ce887f	DeepAndShallowEmbeddings: initial, simpler example	2016-04-10 18:53:36 -04:00
Adam Chlipala	11e1c74b1c	DeepAndShallowEmbeddings: proof automation for examples	2016-04-10 17:01:03 -04:00
Adam Chlipala	4849bf22a2	DeepAndShallowEmbeddings: example of a derived program form	2016-04-10 16:33:32 -04:00
Adam Chlipala	9330f3714e	DeepAndShallowEmbeddings: adding failure	2016-04-10 15:38:47 -04:00
Adam Chlipala	290fec1e5b	DeepAndShallowEmbeddings: Deep	2016-04-10 15:10:56 -04:00
Adam Chlipala	01d550e4b0	DeepAndShallowEmbeddings: ran some code in OCaml	2016-04-10 13:48:58 -04:00