16 commits

Author	SHA1	Message	Date
Adam Chlipala	c502399de4	Separate out library code with its own license	2020-03-17 09:22:06 -04:00
Adam Chlipala	5a28d4fe6a	Replace omega with lia	2020-02-08 14:41:07 -05:00
Adam Chlipala	152b90e9ef	Merge	2020-02-02 17:19:40 -05:00
Adam Chlipala	89f21b8533	First phase of update for Coq 8.10	2020-02-02 17:16:19 -05:00
Adam Chlipala	e032ab4240	Update for Coq 8.9	2019-03-04 11:23:01 -05:00
Adam Chlipala	1ee699431c	Change ProofByReflection to work in Coq 8.6.1	2017-11-18 10:43:08 -05:00
Adam Chlipala	a9ba30076d	Merge	2017-03-18 20:20:23 -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
Adam Chlipala	06b5592c89	Ignore .coq-native	2016-02-22 10:36:30 -05:00
Peng Wang	08f9417302	Added .dir-locals.el in .gitignore	2016-02-03 12:49:16 -05:00
Adam Chlipala	7e99e09b81	Publishing to web	2016-02-02 13:53:00 -05:00
Adam Chlipala	f8945106da	Start of BasicSyntax code	2015-12-31 15:44:34 -05:00
Adam Chlipala	e5898976ab	Fleshed out intro	2015-12-31 14:40:01 -05:00
Adam Chlipala	71d8c98936	Book skeleton, based on amsmath template	2015-12-31 13:50:15 -05:00