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
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
