| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
As before, add a `bitwise as` tactic notation.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
All that really needed to be done was add an explicit intro before
nzinduct, but all the issues in this file could be fixed by moving n m p
before the colon, and I couldn't stop my self.
|
|
specific format.
Reviewed-by: ejgallego
|
|
Reviewed-by: SkySkimmer
|
|
|
|
Reviewed-by: ppedrot
|
|
Evarconv.apply_on_subterm
Reviewed-by: mattam82
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
I know higher-order mutable state shared across call sites is a staple of
Matthieu's style, but it is a footgun begging to be abused.
|
|
Instead of repeatedly checking for evars to appear in a term, we perform
the search in one single pass. This slowdown was observed in fiat-crypto.
This is still a naive algorithm though, since we recompute the set of evars
for each subterm. This is thus quadratic.
|
|
Reviewed-by: jfehrle
Ack-by: ppedrot
|
|
|
|
|
|
-> "constr"
Reviewed-by: herbelin
Ack-by: Zimmi48
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: maximedenes
Reviewed-by: Matafou
Ack-by: ejgallego
|
|
Reviewed-by: jfehrle
Ack-by: Blaisorblade
Ack-by: herbelin
|
|
Update doc/sphinx/language/core/primitive.rst
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
Add persistent data structure
Update doc/sphinx/language/core/primitive.rst
Co-authored-by: Hugo Herbelin <herbelin@users.noreply.github.com>
Update doc/sphinx/language/core/primitive.rst
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
Update doc/sphinx/language/core/primitive.rst
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: jfehrle
|
|
I believe this renaming makes it easier for new contributors to discover
the code of `ring`.
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: SkySkimmer
|
|
|
