index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
ltac2_plugin.mlpack
Age
Commit message (
Collapse
)
Author
2017-11-06
Generalize the use of repr in Tac2stdlib.
Pierre-Marie Pédrot
2017-10-27
Stubs for goal matching: quotation and matching function.
Pierre-Marie Pédrot
2017-09-14
Moving valexpr definition to Tac2ffi.
Pierre-Marie Pédrot
2017-09-08
Fix coq/ltac2#22: Argument to Tactic_failure should be printed.
Pierre-Marie Pédrot
We implement a printer for toplevel values and use it for exceptions in particular.
2017-09-06
Moving Tac2ffi before Tac2interp.
Pierre-Marie Pédrot
2017-08-29
Rolling our own dynamic types for Ltac2.
Pierre-Marie Pédrot
This prevents careless confusions with generic arguments from Coq.
2017-08-18
Laxer dependencies between file and link reordering.
Pierre-Marie Pédrot
2017-08-02
Tentatively implementing apply.
Pierre-Marie Pédrot
2017-08-01
Adding new scopes for standard Ltac structures.
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
2017-07-24
Turning the ltac2 subfolder into a standalone plugin.
Pierre-Marie Pédrot
