aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* rename-everythingGravatar Andres Erbsen2017-04-06
* remove unused filesGravatar Andres Erbsen2017-04-06
* reduce BaseSystemGravatar Andres Erbsen2017-04-06
* start removing BaseSystemGravatar Andres Erbsen2017-04-06
* git rm -rf src/BoundedArithmetic/Double/Repeated/ (and users)Gravatar Andres Erbsen2017-04-06
* do not import BaseSystem unnecessarilyGravatar Andres Erbsen2017-04-06
* remove Encoding stuffGravatar Andres Erbsen2017-04-06
* do not use VerdiTactics in files we plan to keepGravatar Andres Erbsen2017-04-06
* git rm -rf src/AssemblyGravatar Andres Erbsen2017-04-06
* note running time of Weierstrass associativity QedGravatar Andres Erbsen2017-04-06
* Finish fixing Glue to actually handle ladderstepGravatar Jason Gross2017-04-06
* Export ClearAll in TacticsGravatar Jason Gross2017-04-06
* More vigorous clearing in unify_transformed_rhs_abstract_tacGravatar Jason Gross2017-04-06
* Unfold tuples in do_reifyGravatar Jason Gross2017-04-06
* Add clear_allGravatar Jason Gross2017-04-06
* Support Z.oppGravatar Jason Gross2017-04-05
* Even better reify failure messagesGravatar Jason Gross2017-04-05
* make elliptic curve proofs faster and split them into filesGravatar Andres Erbsen2017-04-05
* Fix a commented out importGravatar Jason Gross2017-04-05
* Use tactics from MoveLetIn in integration testGravatar Jason Gross2017-04-05
* Better error message in reificationGravatar Jason Gross2017-04-05
* Don't clutter up typeclass log with cidtacGravatar Jason Gross2017-04-05
* Fix a major inefficiency in reify_context_variablesGravatar Jason Gross2017-04-05
* reify_context_variables in ReflectiveTacticsGravatar Jason Gross2017-04-05
* Always unfold [interp_base_type] in reify_context_variablesGravatar Jason Gross2017-04-05
* Handle context variables in ReifyGravatar Jason Gross2017-04-05
* Fix transparent assert by to respect namesGravatar Jason Gross2017-04-05
* Add TransparentAssertGravatar Jason Gross2017-04-05
* Glue pipeline: Curry and type-reify context varsGravatar Jason Gross2017-04-05
* Remove bad [Local]Gravatar Jason Gross2017-04-05
* Actually add ChangeInAllGravatar Jason Gross2017-04-05
* Add Tactics.ChangeInAllGravatar Jason Gross2017-04-05
* Fix bug in change_with_curriedGravatar Jason Gross2017-04-05
* When currying, change with curried form in *Gravatar Jason Gross2017-04-05
* Update glue reflective pipeline to handle ladderstepGravatar Jason Gross2017-04-05
* Add Tactics.MoveLetInGravatar Jason Gross2017-04-05
* Set Suggest Proof Using seems to have been missing one?Gravatar Jason Gross2017-04-04
* Fix some documentationGravatar Jason Gross2017-04-04
* Rework second 2/3 of the glue: work on ladderstepGravatar Jason Gross2017-04-04
* Add Tactics.PrintContextGravatar Jason Gross2017-04-04
* Accurate Proof using for commutative_groupGravatar Jason Gross2017-04-04
* Fix WeierstrassCurveTheorems.vGravatar Jason Gross2017-04-04
* Work around bug #5453Gravatar Jason Gross2017-04-04
* Add [Proof using] to most proofsGravatar Jason Gross2017-04-04
* Move sigma MapProjections to a separate fileGravatar Jason Gross2017-04-04
* Add Proof using Type to WCT for faster "coqc" -quick -q -R "src" Crypto -R ...Gravatar Jason Gross2017-04-04
* Add Tuple.map_ProperGravatar Jason Gross2017-04-03
* Use a more robust way of saving context definitions in IntegrationTestGravatar Jason Gross2017-04-03
* Use dlet in MontgomeryXGravatar Jason Gross2017-04-03
* More fine-grained tactic importsGravatar Jason Gross2017-04-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-22 08:28:13 +0000