aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Add interp_reify_and_let_binds_baseGravatar Jason Gross2018-10-25
* Add interp_reify_as_interpGravatar Jason Gross2018-10-24
* Add GallinaReify.reify_as_interpGravatar Jason Gross2018-10-24
* Add rawexpr_equiv_expr_to_type_of_rawexprGravatar Jason Gross2018-10-23
* Add a horribly manual proof of app_forall_vars_under_forall_vars_relation1Gravatar Jason Gross2018-10-23
* Add some equality lemmas about Positive{Map,Set}Gravatar Jason Gross2018-10-23
* Add under_with_unification_resultT'_relation1_gen_alwaysGravatar Jason Gross2018-10-23
* Add related1_app_type_of_list_under_type_of_list_relation1_cpsGravatar Jason Gross2018-10-23
* Update rewriter correctness conditionGravatar Jason Gross2018-10-23
* Tactic-in-term: ensuring same scope for all occurrences of a notation variable.Gravatar Hugo Herbelin2018-10-23
* Add placeholder rewrite rules for rewriting after boundsGravatar Jason Gross2018-10-14
* Minor changes to rewriterGravatar Jason Gross2018-10-14
* Guarantee that casting always returns inrangeGravatar Jason Gross2018-10-12
* Add some zrange lemmasGravatar Jason Gross2018-10-11
* Parameterize rewriter proofs over cast-outside-of-range behaviorGravatar Jason Gross2018-10-11
* Add interp-correctness condition for rewriterGravatar Jason Gross2018-10-11
* Export more tactics in Tactics.vGravatar Jason Gross2018-10-10
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 08:48:03 +0000