aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Rename [normalize_commutative_identifier] file to match tactic nameGravatar Jason Gross2018-10-10
* Add [normalize_commutative_identifier] tacticGravatar Jason Gross2018-10-10
* Add some natutil and listutil lemmasGravatar Jason Gross2018-10-10
* Restore Redirect in comment blocksGravatar Jason Gross2018-10-09
* Remove [Redirect] to absolute pathsGravatar Andres Erbsen2018-10-09
* Fix a bad rewrite ruleGravatar Jason Gross2018-10-09
* Add map_update_nth_extGravatar Jason Gross2018-10-09
* Add under_with_unification_resultT_relation_heteroGravatar Jason Gross2018-10-09
* Use [reify_list] in [smart_Literal]Gravatar Jason Gross2018-10-09
* Add ListUtil.ForallInGravatar Jason Gross2018-10-09
* Compatibility with Coq PR#8457Gravatar Frédéric Besson2018-10-04
* Add some more lemmas about generated stuffGravatar Jason Gross2018-10-02
* Adapt to Coq's PR#8555Gravatar Maxime Dénès2018-10-02
* Add more gen ident proofsGravatar Jason Gross2018-10-01
* Add pattern.ident.to_typedGravatar Jason Gross2018-10-01
* Add a few rewriter definitionsGravatar Jason Gross2018-10-01
* Support type variables in patterns in the rewriterGravatar Jason Gross2018-09-29
* Fix and prove bounds for fancymachine operationsGravatar jadep2018-09-28
* Add some option bind lemmasGravatar Jason Gross2018-09-27
* Clean up type_beq_to_eq a bitGravatar Jason Gross2018-09-27
* Add more reflect tacticsGravatar Jason Gross2018-09-27
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 20:30:24 +0000