16 commits

Author	SHA1	Message	Date
Adam Chlipala	c611524a96	Prevent more warnings for Coq 8.10	2020-02-08 15:15:38 -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	c5600db874	SubsetTypes	2017-03-21 19:27:36 -04:00
Adam Chlipala	c8322773a4	Simplify sets in hypotheses, too	2017-03-12 21:27:59 -04:00
Adam Chlipala	cd2a474d5d	Fix a performance bug in model_check	2017-03-07 14:59:56 -05:00
Adam Chlipala	1e7c33f0a9	Optimizing tactics for faster state-space exploration	2017-03-05 20:46:53 -05:00
Adam Chlipala	132ac914e4	Sets: change parsing precedence	2016-04-26 13:46:48 -04:00
Adam Chlipala	3b7d898b0f	SharedMemory: commutes_sound	2016-04-22 19:11:42 -04:00
Adam Chlipala	f37e9ba34d	SharedMemory: model-checking example, after tweaking library	2016-04-21 13:42:30 -04:00
Adam Chlipala	2c601b04a0	Fixed to work in Coq 8.4, too	2016-02-18 17:51:58 -05:00
Adam Chlipala	c129d8447e	Some heftier ModelChecking examples	2016-02-14 19:23:26 -05:00
Adam Chlipala	eb50f67c2a	Smarter ModelChecking with a worklist	2016-02-14 17:55:59 -05:00
Adam Chlipala	4371d08696	Set simplification for ModelChecking	2016-02-14 17:33:46 -05:00
Adam Chlipala	c88ae6d484	Start ModelChecking code: checked [factorial_sys]	2016-02-14 17:13:25 -05:00
Adam Chlipala	f8945106da	Start of BasicSyntax code	2015-12-31 15:44:34 -05:00