index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
tac2stdlib.ml
Age
Commit message (
Expand
)
Author
2017-08-25
More bindings to primitive tactics.
Pierre-Marie Pédrot
2017-08-24
Introducing a quotation for global references.
Pierre-Marie Pédrot
2017-08-24
Use references in reduction tactics.
Pierre-Marie Pédrot
2017-08-18
Removing dead code.
Pierre-Marie Pédrot
2017-08-05
Exporting more reduction functions.
Pierre-Marie Pédrot
2017-08-05
Exporting the rewrite tactic.
Pierre-Marie Pédrot
2017-08-04
Adding the induction and destruct tactics.
Pierre-Marie Pédrot
2017-08-02
Tentatively implementing apply.
Pierre-Marie Pédrot
2017-08-02
Merging the e/- variants of primitive tactics.
Pierre-Marie Pédrot
2017-08-02
Adding new notations.
Pierre-Marie Pédrot
2017-08-02
Fixup reification of egeneralize.
Pierre-Marie Pédrot
2017-08-01
More primitive tactics.
Pierre-Marie Pédrot
2017-08-01
Introducing the all-mighty intro-patterns.
Pierre-Marie Pédrot
2017-08-01
Binding more primitive tactics.
Pierre-Marie Pédrot
2017-07-30
Exporting more internals from Coq implementation.
Pierre-Marie Pédrot
2017-07-28
Parameterizing FFI functions for parameterized types.
Pierre-Marie Pédrot
2017-07-28
Moving the Ltac2 FFI to a separate file.
Pierre-Marie Pédrot
2017-07-26
Exporting some basic tactics from Ltac1.
Pierre-Marie Pédrot
