aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* fix typoGravatar jadep2019-04-03
* remove unnecessary imports from Primitives.vGravatar jadep2019-04-03
* fix up imports in SmallExamples.vGravatar jadep2019-04-03
* update import statementsGravatar jadep2019-04-03
* rename some thingsGravatar jadep2019-04-03
* fix imports and qualifiers so everything buildsGravatar jadep2019-04-03
* remove extraneous module identifiersGravatar jadep2019-04-03
* update _CoqProject, fix indentations, and prune dependencies of new Arithmeti...Gravatar jadep2019-04-03
* split up Arithmetic (imports etc. not yet fixed, does not build)Gravatar jadep2019-04-03
* Add Z.combine_at_bitwidthGravatar Jason Gross2019-04-02
* Factor out rewriter rulesGravatar Jason Gross2019-03-31
* Fix a non-terminated commentGravatar Jason Gross2019-03-31
* Add some comments based on CR requestsGravatar Jason Gross2019-03-31
* Fix issue with refolding in eapply in < 8.9Gravatar Jason Gross2019-03-31
* Finish reifying list lemmasGravatar Jason Gross2019-03-31
* Add constr_fail and constr_fail_withGravatar Jason Gross2019-03-31
* improve zero_bounds tacticGravatar jadep2019-03-26
* add some hints to the global databasesGravatar jadep2019-03-26
* 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
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-11 13:03:51 +0000