aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Add match commutation lemmasGravatar Jason Gross2017-01-23
* Preserve names in invert_expr_substGravatar Jason Gross2017-01-23
* Make invert_expr_subst not loopGravatar Jason Gross2017-01-23
* Fix invert_expr_substGravatar Jason Gross2017-01-23
* Better invert_exprGravatar Jason Gross2017-01-23
* Minor additionsGravatar Jason Gross2017-01-23
* Fix a typoGravatar Jason Gross2017-01-23
* Add invert_expr_substGravatar Jason Gross2017-01-23
* Allow inversion on wff if either side is not a varGravatar Jason Gross2017-01-23
* Add transparent equality proofs for fixed wordTGravatar Jason Gross2017-01-21
* Revert "Fix a missing qualification"Gravatar Jason Gross2017-01-21
* Fix a missing qualificationGravatar Jason Gross2017-01-21
* Move weqb_hetero to Bedrock.WordGravatar Jason Gross2017-01-21
* Add weqb_heteroGravatar Jason Gross2017-01-21
* Add split_andb tacticGravatar Jason Gross2017-01-21
* Update notations from zetabaseGravatar Jason Gross2017-01-19
* Add ZUtil lemma from zetabaseGravatar Jason Gross2017-01-19
* Remove the Const constructor of exprfGravatar Jason Gross2017-01-19
* Make f_equal2 transparent in equality proofGravatar Jason Gross2017-01-19
* Add nat_beq_to_eqGravatar Jason Gross2017-01-19
* Split out Reflection.Equality, change Tflat implicit argumentGravatar Jason Gross2017-01-19
* Fix infinite loop in destruct_rewrite_sumboolGravatar Jason Gross2017-01-17
* Fix changed qualified tactic nameGravatar Jason Gross2017-01-17
* More fine-grained util tactic filesGravatar Jason Gross2017-01-17
* Use match in curry2; this gives better reificationGravatar Jason Gross2017-01-15
* Add curry.vGravatar Jason Gross2017-01-15
* More universe fixesGravatar Jason Gross2017-01-15
* Fix an issue with universesGravatar Jason Gross2017-01-15
* Add ApplicationRelationsGravatar Jason Gross2017-01-10
* Add Syntax.tuple_mapGravatar Jason Gross2017-01-09
* Add >>> reserved notationGravatar Jason Gross2017-01-09
* Add Zmod_to_equiv_moduloGravatar Jason Gross2017-01-09
* copy_boundsGravatar Jason Gross2017-01-07
* Add reified LadderStep without carriesGravatar Jason Gross2017-01-07
* Add ladderstep_other_assocGravatar Jason Gross2017-01-07
* Revert "Add apply10"Gravatar Jason Gross2017-01-07
* Add apply10Gravatar Jason Gross2017-01-07
* copy_boundsGravatar Jason Gross2017-01-07
* Add Common10_4OpGravatar Jason Gross2017-01-07
* Add Expr10_4OpGravatar Jason Gross2017-01-07
* Add i10top_correct_and_boundedGravatar Jason Gross2017-01-07
* Add appify10Gravatar Jason Gross2017-01-07
* Add more generic ladderstepGravatar Jason Gross2017-01-07
* Better word operationsGravatar Jason Gross2017-01-03
* Add word versions of ModularBaseSystemListZOperationsGravatar Jason Gross2017-01-03
* Add ZToWord,wordToZGravatar Jason Gross2017-01-03
* Add fixed word size definitionsGravatar Jason Gross2017-01-03
* Fixes for Coq 8.4Gravatar Jason Gross2017-01-03
* Add src/Reflection/MapCastWithCastOp.vGravatar Jason Gross2017-01-01
* Remove [Print]Gravatar Jason Gross2017-01-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 08:25:09 +0000