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-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-10-07
Remove unused warnings.
Pierre-Marie Pédrot
2017-10-01
Abstracting away the implementation of value representations.
Pierre-Marie Pédrot
2017-10-01
Using Ltac2 native closures in some tactic APIs.
Pierre-Marie Pédrot
2017-09-30
Abstracting away the primitive functions on valexpr datatype.
Pierre-Marie Pédrot
2017-09-15
Phantom type for typed closures.
Pierre-Marie Pédrot
2017-09-14
Abstracting away the type of arities and ML tactics.
Pierre-Marie Pédrot
2017-09-14
Moving valexpr definition to Tac2ffi.
Pierre-Marie Pédrot
2017-09-14
Explicit arity for closures.
Pierre-Marie Pédrot
2017-09-09
Moving Ltac2 backtraces to the Exninfo mechanism.
Pierre-Marie Pédrot
2017-09-06
Using higher-order representation for closures.
Pierre-Marie Pédrot
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
