index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
_CoqProject
Commit message (
Expand
)
Author
Age
*
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
*
Add ContextProperties
Jason Gross
2017-03-14
*
Move ContextOk to ContextDefinitions
Jason Gross
2017-03-14
*
Add lemma about wff and interpf of Named
Jason Gross
2017-03-14
*
Add FMapContext, PositiveContext
Jason Gross
2017-03-08
*
Separated out specific test cases for new base system
jadep
2017-03-04
*
remove dangling file...
Andres Erbsen
2017-03-02
*
deleted src/Specific/GF25519ExtendedAddCoordinates.v
Andres Erbsen
2017-03-02
*
fix src/Specific/GF25519Reflective/Reified/AddCoordinates.v
Andres Erbsen
2017-03-02
*
PrimeFieldTheorems: inv for isomorphic fields
Andres Erbsen
2017-03-02
*
address some code review comments
Andres Erbsen
2017-03-02
*
Weierstrass curve is a group
Andres Erbsen
2017-03-02
*
split the algebra library; use fsatz more
Andres Erbsen
2017-03-02
*
Switch to fully uncurried form for reflection
Jason Gross
2017-03-01
*
Update _CoqProject
Jason Gross
2017-02-27
*
speed up NewBaseystem synthesis
Andres Erbsen
2017-02-23
*
Add BoundsInterpretations
Jason Gross
2017-02-23
*
Moved N lemmas from Ed25519 and IterAssocOp into new NUtil file
jadep
2017-02-22
*
Merge new base system (#112)
jadephilipoom
2017-02-22
*
Add various reflection improvements, boundbycast
Jason Gross
2017-02-21
*
Add MapCastInterp
Jason Gross
2017-02-16
*
Add InterpByIsoProofs
Jason Gross
2017-02-16
*
Add InterpByIso
Jason Gross
2017-02-16
*
make update-_CoqProject
Jason Gross
2017-02-15
*
Add rudimentary Java and C notation files, display
Jason Gross
2017-02-15
*
Add partially finished MapCastWf
Jason Gross
2017-02-14
*
Add src/Reflection/BoundByCastWf.v
Jason Gross
2017-02-14
*
Add SmartBoundWf
Jason Gross
2017-02-14
*
Add InlineCastInterp.v
Jason Gross
2017-02-13
*
Add InlineCastWf
Jason Gross
2017-02-13
*
Add SmartCast{Interp,Wf}
Jason Gross
2017-02-13
*
Split up BoundByCast
Jason Gross
2017-02-13
*
Add EtaInterp, EtaWf
Jason Gross
2017-02-10
*
Add Reflection/Eta.v
Jason Gross
2017-02-10
*
Add files for constant reflective notations
Jason Gross
2017-02-10
*
added ZToRing to _CoqProject
jadep
2017-02-09
*
Factor things into BoundByCast.v
Jason Gross
2017-02-08
*
Simpler version of MapCast
Jason Gross
2017-02-08
*
Split up Reflection/Z/Syntax and make it smaller
Jason Gross
2017-02-02
*
Add invert_op
Jason Gross
2017-02-01
*
Add invert_expr
Jason Gross
2017-02-01
*
Split off unique {pose,assert}
Jason Gross
2017-01-31
*
Add Util.Sumbool
Jason Gross
2017-01-30
*
Split off some bits of Reflection.Syntax
Jason Gross
2017-01-26
*
Update _CoqProject
Jason Gross
2017-01-21
*
Add LetInMonad to _CoqProject
Jason Gross
2017-01-19
*
Remove the Const constructor of exprf
Jason Gross
2017-01-19
[next]