7 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	796fc8d64c	Noticed one invariant in HoareLogic was more complex than required	2021-04-12 16:03:38 -04:00
Adam Chlipala	899b3dee24	Revising for this week's lectures	2021-04-11 13:32:38 -04: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	26365924ef	DependentInductiveTypes_template	2018-04-10 18:24:03 -04:00