aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
Commit message (Expand)AuthorAge
...
* split the algebra library; use fsatz moreGravatar Andres Erbsen2017-03-02
* Switch to fully uncurried form for reflectionGravatar Jason Gross2017-03-01
* Update _CoqProjectGravatar Jason Gross2017-02-27
* speed up NewBaseystem synthesisGravatar Andres Erbsen2017-02-23
* Add BoundsInterpretationsGravatar Jason Gross2017-02-23
* Moved N lemmas from Ed25519 and IterAssocOp into new NUtil fileGravatar jadep2017-02-22
* Merge new base system (#112)Gravatar jadephilipoom2017-02-22
* Add various reflection improvements, boundbycastGravatar Jason Gross2017-02-21
* Add MapCastInterpGravatar Jason Gross2017-02-16
* Add InterpByIsoProofsGravatar Jason Gross2017-02-16
* Add InterpByIsoGravatar Jason Gross2017-02-16
* make update-_CoqProjectGravatar Jason Gross2017-02-15
* Add rudimentary Java and C notation files, displayGravatar Jason Gross2017-02-15
* Add partially finished MapCastWfGravatar Jason Gross2017-02-14
* Add src/Reflection/BoundByCastWf.vGravatar Jason Gross2017-02-14
* Add SmartBoundWfGravatar Jason Gross2017-02-14
* Add InlineCastInterp.vGravatar Jason Gross2017-02-13
* Add InlineCastWfGravatar Jason Gross2017-02-13
* Add SmartCast{Interp,Wf}Gravatar Jason Gross2017-02-13
* Split up BoundByCastGravatar Jason Gross2017-02-13
* Add EtaInterp, EtaWfGravatar Jason Gross2017-02-10
* Add Reflection/Eta.vGravatar Jason Gross2017-02-10
* Add files for constant reflective notationsGravatar Jason Gross2017-02-10
* added ZToRing to _CoqProjectGravatar jadep2017-02-09
* Factor things into BoundByCast.vGravatar Jason Gross2017-02-08
* Simpler version of MapCastGravatar Jason Gross2017-02-08
* Split up Reflection/Z/Syntax and make it smallerGravatar Jason Gross2017-02-02
* Add invert_opGravatar Jason Gross2017-02-01
* Add invert_exprGravatar Jason Gross2017-02-01
* Split off unique {pose,assert}Gravatar Jason Gross2017-01-31
* Add Util.SumboolGravatar Jason Gross2017-01-30
* Split off some bits of Reflection.SyntaxGravatar Jason Gross2017-01-26
* Update _CoqProjectGravatar Jason Gross2017-01-21
* Add LetInMonad to _CoqProjectGravatar Jason Gross2017-01-19
* Remove the Const constructor of exprfGravatar Jason Gross2017-01-19
* Split out Reflection.Equality, change Tflat implicit argumentGravatar Jason Gross2017-01-19
* More fine-grained util tactic filesGravatar Jason Gross2017-01-17
* Add curry.vGravatar Jason Gross2017-01-15
* Add ApplicationRelationsGravatar Jason Gross2017-01-10
* update-_CoqProjectGravatar Jason Gross2017-01-07
* Add reified LadderStep without carriesGravatar Jason Gross2017-01-07
* Revert "Add apply10"Gravatar Jason Gross2017-01-07
* copy_boundsGravatar Jason Gross2017-01-07
* Add fixed word size definitionsGravatar Jason Gross2017-01-03
* Add src/Reflection/MapCastWithCastOp.vGravatar Jason Gross2017-01-01
* Redo MultiSizeTest with generic frameworkGravatar Jason Gross2017-01-01
* Add generic code for MultiSizeTestGravatar Jason Gross2017-01-01
* make update-_CoqProjectGravatar Jason Gross2016-12-26
* Add WfInversionGravatar Jason Gross2016-12-03
* Move things to ExprInversionGravatar Jason Gross2016-12-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-14 03:51:09 +0000