aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Also inline Z_cast thingsGravatar Jason Gross2018-11-01
* Add some zrange lemmasGravatar Jason Gross2018-11-01
* Make pairs work in Z_cast2Gravatar Jason Gross2018-11-01
* Export ZRange operation notationsGravatar Jason Gross2018-11-01
* Add zrange notationsGravatar Jason Gross2018-11-01
* Fix a thing broken by previous commitGravatar Jason Gross2018-11-01
* Add more reserved notationsGravatar Jason Gross2018-11-01
* Add more zrange operationsGravatar Jason Gross2018-11-01
* Remove dead codeGravatar Jason Gross2018-11-01
* Tactic-in-term: ensuring same scope for all occurrences of a notation variable.Gravatar Hugo Herbelin2018-11-01
* Fix a bug in 8.7 compilationGravatar Jason Gross2018-10-30
* Refactor/generalize some pipeline definitions/proofsGravatar Jason Gross2018-10-30
* Remove duplicate abstractionGravatar Jasper Hugunin2018-10-29
* Add PositiveSet FactsGravatar Jason Gross2018-10-29
* Add eqlistA_eq_iffGravatar Jason Gross2018-10-29
* Add split_contravariant_orGravatar Jason Gross2018-10-29
* Add ex_eq_and tacticGravatar Jason Gross2018-10-29
* Add some lemmas about ex, and, eqGravatar Jason Gross2018-10-29
* Stricter check on types in the rewriterGravatar Jason Gross2018-10-29
* Add subst_relaxGravatar Jason Gross2018-10-29
* Add subst_Some_subst_default, subst_relax_evmGravatar Jason Gross2018-10-29
* Fix a proofGravatar Jason Gross2018-10-28
* Add an extra check in the rewriterGravatar Jason Gross2018-10-28
* Improve cps_id tactics, add add_var_types_cps_id, unify_extracted_cps_id tacticsGravatar Jason Gross2018-10-28
* Fix a bug in ensure_complex_continuationGravatar Jason Gross2018-10-28
* Add CPSId tacticsGravatar Jason Gross2018-10-28
* Add unify_extracted_cps_idGravatar Jason Gross2018-10-28
* Add app_lam_type_of_listGravatar Jason Gross2018-10-25
* Add under_forall_vars_relation1_lam_forall_vars, remove forall2_type_of_list_...Gravatar Jason Gross2018-10-25
* Remove value'_interp_related1Gravatar Jason Gross2018-10-25
* Add value_interp_related1Gravatar Jason Gross2018-10-25
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 22:02:03 +0000