| Commit message (Expand) | Author | Age |
* | More fine-grained tactic imports | Jason Gross | 2017-04-03 |
* | Split off liftn_sig, add lift{3,4}_sig | Jason Gross | 2017-04-03 |
* | make update-_CoqProject | Jason Gross | 2017-04-03 |
* | Add an initial stab at doing the pipeline mostly in Gallina | Jason Gross | 2017-04-03 |
* | Rename PreDefinitions to OutputType | Jason Gross | 2017-04-03 |
* | An approximately first stab DeBruijn word-size-sel | Jason Gross | 2017-04-03 |
* | Remove old reflective pipeline, making way the new | Jason Gross | 2017-04-03 |
* | Remove everything after the individual reified ops | Jason Gross | 2017-04-03 |
* | Add UnifyAbstractReflexivity tactics | Jason Gross | 2017-04-03 |
* | Add Tactics.EvarExists | Jason Gross | 2017-04-02 |
* | Add Util.SigmaAssoc | Jason Gross | 2017-04-02 |
* | Remove the bits of the new reflective pipeline in master | Jason Gross | 2017-04-02 |
* | Remove all the .v files in SpecificGen | Jason Gross | 2017-04-02 |
* | Add PreDefinitions pipeline file | Jason Gross | 2017-04-02 |
* | Add Z instantiations of InlineConst | Jason Gross | 2017-04-02 |
* | Add Z.Bounds.MapCastByDeBruijn instantiation | Jason Gross | 2017-04-02 |
* | Add Z instantiation of MapCastByDeBruijnInterp | Jason Gross | 2017-04-02 |
* | Add an initial glue file in the pipeline, no option in bounds | Jason Gross | 2017-04-01 |
* | Split off BoundedWord.v from IntegrationTest.v | Jason Gross | 2017-04-01 |
* | Add RenameBinders | Jason Gross | 2017-04-01 |
* | Add wf proof for arithmetic simplifer | Jason Gross | 2017-04-01 |
* | Add an arithmetic simplifier | Jason Gross | 2017-04-01 |
* | Add correctness of Rewriter | Jason Gross | 2017-04-01 |
* | Add Reflection/Rewriter.v | Jason Gross | 2017-04-01 |
* | Split out Tactics.SubstLet | Jason Gross | 2017-04-01 |
* | Add a bounds relaxation lemma | Jason Gross | 2017-03-31 |
* | Add [etransitivity y], [etransitivity_rev] tactics | Jason Gross | 2017-03-31 |
* | use improved fsatz on various elliptic curve things | Andres Erbsen | 2017-03-31 |
* | Start instantiating MapCastByDeBruijn in Z/ | Jason Gross | 2017-03-30 |
* | Don't linearize and eta in MapCastByDeBruijn | Jason Gross | 2017-03-30 |
* | Rename Bounds to ZRange, use Prop, not bool | Jason Gross | 2017-03-30 |
* | Add a file dedicated to the definition of Z bounds | Jason Gross | 2017-03-30 |
* | Add Z.FoldTypes.{Min,Max}TypeUsed | Jason Gross | 2017-03-28 |
* | Add FoldTypes | Jason Gross | 2017-03-28 |
* | make update-_CoqProject | Jason Gross | 2017-03-28 |
* | Added saturated arithmetic file, including [compact] code and proof | jadep | 2017-03-24 |
* | Add aborted CompileProperties | Jason Gross | 2017-03-22 |
* | Add aborted MapCastByDeBruijnWf | Jason Gross | 2017-03-19 |
* | Add MapCastWf | Jason Gross | 2017-03-19 |
* | Most of the way towards a complete MapCastCorrect | Jason Gross | 2017-03-19 |
* | Add Named/PositiveContext/DefaultsProperties.v | Jason Gross | 2017-03-19 |
* | Split up ContextProperties | Jason Gross | 2017-03-19 |
* | Add IdContext | Jason Gross | 2017-03-17 |
* | Add MapCastByDeBruijn on PHOAS syntax | Jason Gross | 2017-03-17 |
* | Add aborted in-process compile-{wf,interp} proofs | Jason Gross | 2017-03-17 |
* | Add a Named version of MapCast | Jason Gross | 2017-03-17 |
* | Add NameUtilProperties | Jason Gross | 2017-03-14 |
* | Add InterpretToPHOASInterp | Jason Gross | 2017-03-14 |
* | Add Wf_InterpToPHOAS | Jason Gross | 2017-03-14 |
* | Add InterpretToPHOAS | Jason Gross | 2017-03-14 |