index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
tac2expr.mli
Age
Commit message (
Expand
)
Author
2018-06-18
Adapt to Coq's PR #7797 (removal of reference).
Maxime Dénès
2018-06-18
Fixing a batch of deprecation warnings.
Pierre-Marie Pédrot
2018-03-10
[coq] Adapt to coq/coq#6831.
Emilio Jesus Gallego Arias
2017-11-02
Moving pattern type constraints to pattern AST.
Pierre-Marie Pédrot
2017-10-27
Adding a command to evaluate Ltac2 expressions.
Pierre-Marie Pédrot
2017-10-07
Remove unused warnings.
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-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-09-03
Uniform handling of locations in the various AST.
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
Removing dead code for handling of array litterals.
Pierre-Marie Pédrot
2017-08-27
Do not reuse the Val.t type in toplevel values.
Pierre-Marie Pédrot
2017-08-27
Introducing rebindable toplevel definitions.
Pierre-Marie Pédrot
2017-08-24
Removing dead code about arrays in the AST.
Pierre-Marie Pédrot
2017-08-24
Rely on quoting for lists instead of hardwiring it in the AST.
Pierre-Marie Pédrot
2017-08-07
Introducing grammar-free tactic notations.
Pierre-Marie Pédrot
2017-07-28
Allowing generic patterns in let-bindings.
Pierre-Marie Pédrot
2017-07-27
Factorizing code for constructors and tuples.
Pierre-Marie Pédrot
2017-07-27
Cleaning up code in internalization.
Pierre-Marie Pédrot
2017-07-26
Ensuring that inductive constructors are always capitalized.
Pierre-Marie Pédrot
2017-07-25
Generalizing patterns in fun bindings.
Pierre-Marie Pédrot
2017-07-24
Turning the ltac2 subfolder into a standalone plugin.
Pierre-Marie Pédrot
