index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
tac2ffi.ml
Age
Commit message (
Expand
)
Author
2017-09-06
Parameterizing over parameters in ML functions from Tac2core.
Pierre-Marie Pédrot
2017-09-06
The interp_app function now takes a closure as an argument.
Pierre-Marie Pédrot
2017-09-06
Moving Tac2ffi before Tac2interp.
Pierre-Marie Pédrot
2017-09-06
Introducing abstract data representations.
Pierre-Marie Pédrot
2017-09-04
Quick-and-dirty backtrace mechanism for the interpreter.
Pierre-Marie Pédrot
2017-08-31
Properly handling internal errors from Coq.
Pierre-Marie Pédrot
2017-08-31
Expand the primitive functions on terms.
Pierre-Marie Pédrot
2017-08-29
Centralizing tag declarations.
Pierre-Marie Pédrot
2017-08-29
Rolling our own generic arguments.
Pierre-Marie Pédrot
2017-08-29
Rolling our own dynamic types for Ltac2.
Pierre-Marie Pédrot
2017-08-27
Do not reuse the Val.t type in toplevel values.
Pierre-Marie Pédrot
2017-08-24
Introducing a quotation for global references.
Pierre-Marie Pédrot
2017-08-01
Binding more primitive tactics.
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
