aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection
Commit message (Expand)AuthorAge
* More fine-grained tactic importsGravatar Jason Gross2017-04-03
* Split off liftn_sig, add lift{3,4}_sigGravatar 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
* 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
* clear before abstract so we can handle existentialsGravatar Jason Gross2017-04-02
* Add InterpEtaGravatar Jason Gross2017-04-02
* Remove the bits of the new reflective pipeline in masterGravatar 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
* Rewrite in Op arguments before rewriting in OpGravatar Jason Gross2017-04-01
* Also do eta under lets in Reflection/Eta.vGravatar Jason Gross2017-04-01
* Add an initial glue file in the pipeline, no option in boundsGravatar Jason Gross2017-04-01
* Add back word hex constant notationsGravatar Jason Gross2017-04-01
* Add RenameBindersGravatar Jason Gross2017-04-01
* Add wf proof for arithmetic simpliferGravatar Jason Gross2017-04-01
* Fix a name (sprurious interp)Gravatar Jason Gross2017-04-01
* Add interp proof for arithmetic simplifierGravatar Jason Gross2017-04-01
* Handle inversion of homogenous products in reflective type inversionGravatar Jason Gross2017-04-01
* Add an arithmetic simplifierGravatar Jason Gross2017-04-01
* Add correctness of RewriterGravatar Jason Gross2017-04-01
* Add Reflection/Rewriter.vGravatar Jason Gross2017-04-01
* Alter relax_output_bounds statementGravatar Jason Gross2017-04-01
* Add a bounds relaxation lemmaGravatar Jason Gross2017-03-31
* Fix inversion_base_typeGravatar Jason Gross2017-03-31
* Add inversion_base_type for Z.Syntax.base_typeGravatar Jason Gross2017-03-31
* Add Bounds.is_tighter_thanbGravatar Jason Gross2017-03-31
* Use a better order of arguments for Bounds.is_bounded_byGravatar Jason Gross2017-03-31
* Start instantiating MapCastByDeBruijn in Z/Gravatar Jason Gross2017-03-30
* Reorder arguments to Wf_MapCast for eautoGravatar Jason Gross2017-03-30
* Don't linearize and eta in MapCastByDeBruijnGravatar Jason Gross2017-03-30
* Revert "Update CNotations, JavaNotations"Gravatar Jason Gross2017-03-30
* Update CNotations, JavaNotationsGravatar Jason Gross2017-03-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 18:23:09 +0000