index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
tac2interp.ml
Age
Commit message (
Expand
)
Author
2019-02-20
[coq] Fix OCaml warnings.
Emilio Jesus Gallego Arias
2017-10-07
Remove unused warnings.
Pierre-Marie Pédrot
2017-09-30
Abstracting away the primitive functions on valexpr datatype.
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-07
Fix coq/ltac2#21: Backtraces should print Ltac2 closures.
Pierre-Marie Pédrot
2017-09-07
Communicate the backtrace through the monad.
Pierre-Marie Pédrot
2017-09-06
Using higher-order representation for closures.
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-04
Quick-and-dirty backtrace mechanism for the interpreter.
Pierre-Marie Pédrot
2017-09-04
Closures now wear the constant they originated from.
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-29
Pass Ltac2 variables in a dedicated environment for generic arguments.
Pierre-Marie Pédrot
2017-08-29
Removing dead code for handling of array litterals.
Pierre-Marie Pédrot
2017-08-27
Introducing rebindable toplevel definitions.
Pierre-Marie Pédrot
2017-08-24
Introducing a quotation for global references.
Pierre-Marie Pédrot
2017-07-24
Turning the ltac2 subfolder into a standalone plugin.
Pierre-Marie Pédrot
