15 commits

Author	SHA1	Message	Date
Amanda Liu	1bff5420e2	Update cases tactic to work on N type	2022-02-06 12:47:50 -05:00
Adam Chlipala	f428750fdf	Change notation to remain compatible with multiple Coq versions	2022-01-31 21:02:31 -05:00
Adam Chlipala	d745f0802e	Ported to Coq 8.15	2022-01-29 15:13:09 -05:00
Adam Chlipala	69de20dec8	Revising before class, including with an optimization to the model-checking engine	2020-04-20 11:56:23 -04:00
Adam Chlipala	77f22213d8	Avoid a command only introduced in Coq 8.10, so that 8.9 keeps working	2020-02-10 13:44:35 -05:00
Adam Chlipala	f049d7e824	Scope fix for new N support	2020-02-08 15:18:00 -05:00
Adam Chlipala	0ed668481d	Some N-related library content contributed by Sam Gruetter	2020-02-08 14:56:10 -05:00
Adam Chlipala	89863fd999	Make 'cases' tactic handle disjunction	2020-02-08 14:47:19 -05:00
Adam Chlipala	5a28d4fe6a	Replace omega with lia	2020-02-08 14:41:07 -05:00
Adam Chlipala	89f21b8533	First phase of update for Coq 8.10	2020-02-02 17:16:19 -05:00
Adam Chlipala	a48d85c84c	Improve robustness of set simplification	2018-03-17 19:35:43 -04:00
Adam Chlipala	9550a02a37	Make [sets] tactic more robust to type synonyms	2017-05-14 12:50:18 -04:00
Adam Chlipala	d8e580b331	DependentInductiveTypes	2017-04-02 20:50:10 -04:00
Adam Chlipala	e9e8e6b92b	Add two library lemmas	2017-03-21 21:39:37 -04:00
Adam Chlipala	c5600db874	SubsetTypes	2017-03-21 19:27:36 -04:00