aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Add some lemmas about Bool.reflectGravatar Jason Gross2018-09-27
* Add destruct_head_{False,Empty_set}Gravatar Jason Gross2018-09-27
* Add some Proper lemmas for Option.bindGravatar Jason Gross2018-09-27
* Compatibility after Coq PR#262 (continued).Gravatar Hugo Herbelin2018-09-26
* Compatibility with coq PR #8457Gravatar Frédéric Besson2018-09-25
* Export notations when importing primitiveGravatar Jason Gross2018-09-18
* remove unneeded proofGravatar jadep2018-09-17
* redo all Rows correctness proofs using partition and sanity, remove now-unuse...Gravatar jadep2018-09-17
* remove now-unused nth_default hintsGravatar jadep2018-09-17
* fix up flatten partitioning proofs so that they don't use nth_defaultGravatar jadep2018-09-17
* remove commented-out code that is now clearly unneededGravatar jadep2018-09-17
* Change naming for partitionGravatar jadep2018-09-17
* re-fix syntax so it works on older Coq versionsGravatar jadep2018-09-17
* prove small_div axiomGravatar jadep2018-09-17
* prove eval_mod axiom and clean up eval_div proofGravatar jadep2018-09-17
* use recursive partition to prove eval_div axiomGravatar jadep2018-09-17
* add a recursive definition of partition and prove it equivalentGravatar jadep2018-09-17
* move partition and its proofs to a new module and use it for correctness of C...Gravatar jadep2018-09-17
* change deprecated 'Focus 2' to '2:'Gravatar jadep2018-09-17
* Split out rewrite_with_rule as a separate definitionGravatar Jason Gross2018-09-17
* Actually fix the build for Coq 8.7Gravatar Jason Gross2018-09-17
* Fix 8.7 buildGravatar Jason Gross2018-09-15
* Add nth_error_Proper_eqlistAGravatar Jason Gross2018-09-14
* Add list_elementwise_eqlistAGravatar Jason Gross2018-09-14
* Add PrimitiveSigmaGravatar Jason Gross2018-09-14
* Finish interp proof of abstract interpretationGravatar Jason Gross2018-09-14
* Add option_beq argumentsGravatar Jason Gross2018-09-13
* Add option_beqGravatar Jason Gross2018-09-13
* Remove unused RequireGravatar Vincent Laporte2018-09-12
* Solve two more zrange goalsGravatar Jason Gross2018-09-12
* Make a recording of what zrange proofs are leftGravatar Jason Gross2018-09-12
* Add wf_from_flat_to_flatGravatar Jason Gross2018-09-12
* Help for fixpoint refolding in expr.interpGravatar Jason Gross2018-09-11
* Improve documentation of binariesGravatar Jason Gross2018-09-11
* Add a rudimentary arg parse moduleGravatar Jason Gross2018-08-30
* Do less reduction in split_in_contextGravatar Jason Gross2018-08-29
* Improve speed of do_with_exactly_one_hyp tacticGravatar Jason Gross2018-08-29
* Add src/Util/PER.vGravatar Jason Gross2018-08-29
* Add do_with_exactly_one_hypGravatar Jason Gross2018-08-29
* Do almost all ZRange proofsGravatar Jason Gross2018-08-25
* Minor improvements to various ZUtil things; boundsGravatar Jason Gross2018-08-25
* Fix proofs broken by changes to cc_m proofsGravatar Jason Gross2018-08-24
* Minor rshi tweaksGravatar Jason Gross2018-08-24
* Add some cc_m morphismsGravatar Jason Gross2018-08-24
* Add Z.rshi_correct_fullGravatar Jason Gross2018-08-24
* Add Z.cc_m_eq_fullGravatar Jason Gross2018-08-24
* Add some basic ZRange lemmasGravatar Jason Gross2018-08-24
* Add ZRange.union_commGravatar Jason Gross2018-08-24
* Add a few more zsimplify_const lemmas about shiftGravatar Jason Gross2018-08-24
* Import prim token notations before using themGravatar Jason Gross2018-08-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 23:29:58 +0000