aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
...
* remove Derive to fix 8.7Gravatar jadep2019-03-25
* fix montgomeryGravatar jadep2019-03-25
* remove 2: syntax so I don't break 8.7Gravatar jadep2019-03-25
* fix up a messy proofGravatar jadep2019-03-25
* Move some lemmas to appropriate placesGravatar jadep2019-03-25
* finish proofsGravatar jadep2019-03-25
* Get new Barrett proofs to generate Fancy code as beforeGravatar jadep2019-03-25
* WIPGravatar jadep2019-03-25
* bump submodulesGravatar Andres Erbsen2019-03-22
* remove 8.7 from travis testsGravatar jadep2019-03-21
* Add UnderLets.wf_flat_mapGravatar Jason Gross2019-03-12
* Add UnderLets.wf_of_exprGravatar Jason Gross2019-03-09
* Add some UnderLets wf proofsGravatar Jason Gross2019-03-08
* Standardize list wf thingsGravatar Jason Gross2019-03-08
* Add Forall2_Proper instancesGravatar Jason Gross2019-03-08
* Add Forall2_map_map_iffGravatar Jason Gross2019-03-08
* Add wf_reify_list_Forall2Gravatar Jason Gross2019-03-08
* Allow more reucrsion in wf_safe_t_stepGravatar Jason Gross2019-03-08
* Fix issue with previous commitGravatar Jason Gross2019-03-08
* Add some eq list_rect lemmas to ListUtilGravatar Jason Gross2019-03-08
* Add eager_nth_defaultGravatar Jason Gross2019-03-08
* Remove GlobalTacticalsGravatar Jason Gross2019-03-08
* Fix grepeat tacticGravatar Jason Gross2019-03-08
* Fix gprogress tacticalGravatar Jason Gross2019-03-08
* Add some gtacticsGravatar Jason Gross2019-03-08
* Fix a typoGravatar Jason Gross2019-03-08
* add wf_smart_Literal_eqGravatar Jason Gross2019-03-08
* Add wf_smart_LiteralGravatar Jason Gross2019-03-08
* Add Forall2_forall_In_combine_iffGravatar Jason Gross2019-03-07
* Add wf proofs to UnderLetsProofsGravatar Jason Gross2019-03-07
* Fix hypothesis of UnderLets.list_rect_arrow_interp_relatedGravatar Jason Gross2019-03-07
* Add UnderLets.list_rect_arrow_interp_relatedGravatar Jason Gross2019-03-07
* Add some eq lemmas to ListUtilGravatar Jason Gross2019-03-07
* Also reify List.mapGravatar Jason Gross2019-03-07
* Add list_rect_arrowGravatar Jason Gross2019-03-07
* Add a couple more identifiers to support eager recGravatar Jason Gross2019-03-07
* Add some Proper lemmas to ListUtilGravatar Jason Gross2019-03-07
* Only write to .c files on successGravatar Jason Gross2019-03-07
* Update .out filesGravatar Jason Gross2019-03-07
* Reify most rewrite rulesGravatar Jason Gross2019-03-07
* Fix reification of interpreted identsGravatar Jason Gross2019-03-06
* Add support for reifying fancy identifiersGravatar Jason Gross2019-03-06
* Add reserved notations for \inGravatar Jason Gross2019-03-05
* Allow reifying Z.cast2Gravatar Jason Gross2019-03-05
* Fix unfolding of pattern.base.lookup_defaultGravatar Jason Gross2019-03-05
* Actually fix reification of literalsGravatar Jason Gross2019-03-05
* Revert "Fix reification of literals"Gravatar Jason Gross2019-03-05
* Fix reification of literalsGravatar Jason Gross2019-03-05
* Add UnderLets.flat_mapGravatar Jason Gross2019-03-05
* Fix another instance of reductionGravatar Jason Gross2019-03-04