aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* 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
* Be more fine-grained in WeierstrassCurveTheorems importsGravatar Jason Gross2017-04-03
* Split off liftn_sig, add lift{3,4}_sigGravatar Jason Gross2017-04-03
* Synthesize mul instead of addGravatar Jason Gross2017-04-03
* Work around an anomaly in pretyping/constr_matchingGravatar Jason Gross2017-04-03
* Document some tactics from Jade's pipleine sideGravatar Jason Gross2017-04-03
* Fuse Pipeline.{Composition,ReflectiveTactics}Gravatar Jason Gross2017-04-03
* Fix missing unfold in proofGravatar Jason Gross2017-04-03
* Add missing parenthesesGravatar Jason Gross2017-04-03
* Use projT2_mapGravatar Jason Gross2017-04-03
* Finally, a fully working IntegrationTestGravatar Jason Gross2017-04-03
* WIPGravatar Jason Gross2017-04-03
* WIP on integrationGravatar Jason Gross2017-04-03
* Rework and doc reflective pipeline (more Gallina)Gravatar Jason Gross2017-04-03
* Add an initial stab at doing the pipeline mostly in GallinaGravatar Jason Gross2017-04-03
* Add a bit more documentationGravatar Jason Gross2017-04-03
* Pipeline: reduce away reflective constantsGravatar Jason Gross2017-04-03
* Start adding comments to Pipeline/ReflectiveTactics.vGravatar Jason Gross2017-04-03
* Rename PreDefinitions to OutputTypeGravatar Jason Gross2017-04-03
* Add and update documentation in Pipeline/Glue.vGravatar Jason Gross2017-04-03
* An approximately first stab DeBruijn word-size-selGravatar Jason Gross2017-04-03
* Remove old reflective pipeline, making way the newGravatar Jason Gross2017-04-03
* Remove everything after the individual reified opsGravatar Jason Gross2017-04-03
* Fix parsing issueGravatar Jason Gross2017-04-03
* Add proj2_sig_mapGravatar Jason Gross2017-04-03
* Don't require keeping track of which goals have evars; check that in tacticsGravatar Jason Gross2017-04-03
* Add UnifyAbstractReflexivity tacticsGravatar Jason Gross2017-04-03
* Fix a typoGravatar Jason Gross2017-04-02
* Add projT2_mapGravatar Jason Gross2017-04-02
* Add Tactics.EvarExistsGravatar Jason Gross2017-04-02
* Add Util.SigmaAssocGravatar Jason Gross2017-04-02
* clear before abstract so we can handle existentialsGravatar Jason Gross2017-04-02
* Add ap_transport to Equality.vGravatar Jason Gross2017-04-02
* Add InterpEtaGravatar Jason Gross2017-04-02
* Remove the bits of the new reflective pipeline in masterGravatar Jason Gross2017-04-02
* Remove all the .v files in SpecificGenGravatar Jason Gross2017-04-02
* More extensive comment in NewBaseSystemGravatar Jason Gross2017-04-02
* Work around bug #5434Gravatar Jason Gross2017-04-02
* Coalesce Tuple.pointwise2 and Tuple.fieldwiseGravatar Jason Gross2017-04-02
* Generalize Z.InterpInlineConstGravatar Jason Gross2017-04-02
* Better version of inversion_ProcessedReflectivePackageGravatar Jason Gross2017-04-02
* Add inversion_ProcessedReflectivePackageGravatar Jason Gross2017-04-02
* Add PreDefinitions pipeline fileGravatar Jason Gross2017-04-02
* Add Z instantiations of InlineConstGravatar Jason Gross2017-04-02
* Add Z.Bounds.MapCastByDeBruijn instantiationGravatar Jason Gross2017-04-02
* Add Z instantiation of MapCastByDeBruijnInterpGravatar Jason Gross2017-04-02
* Add reflective_interp rewrite dbGravatar Jason Gross2017-04-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 09:51:17 +0000