index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
tac2entries.ml
Age
Commit message (
Expand
)
Author
2018-03-09
Fix compilation after the change of API in options.
Pierre-Marie Pédrot
2018-03-01
[coq] Adapt to coq/coq#6511
Emilio Jesus Gallego Arias
2017-11-02
Moving pattern type constraints to pattern AST.
Pierre-Marie Pédrot
2017-10-30
Put notations in level 5 by default.
Pierre-Marie Pédrot
2017-10-30
Introducing the change tactic.
Pierre-Marie Pédrot
2017-10-27
Adding a command to evaluate Ltac2 expressions.
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-09-30
Abstracting away the primitive functions on valexpr datatype.
Pierre-Marie Pédrot
2017-09-26
Adding quotations for the assert family of tactics.
Pierre-Marie Pédrot
2017-09-14
Moving valexpr definition to Tac2ffi.
Pierre-Marie Pédrot
2017-09-14
Binding the pose/set family of tactics.
Pierre-Marie Pédrot
2017-09-14
Use a simpler syntax for generalize grammar.
Pierre-Marie Pédrot
2017-09-13
Adding quotations for the generalize tactic.
Pierre-Marie Pédrot
2017-09-09
If backtrace is missing, don't print it.
Pierre-Marie Pédrot
2017-09-09
Moving Ltac2 backtraces to the Exninfo mechanism.
Pierre-Marie Pédrot
2017-09-08
Fix coq/ltac2#22: Argument to Tactic_failure should be printed.
Pierre-Marie Pédrot
2017-09-07
Slightly better printing for anonymous 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-05
Introducing quotations for move locations.
Pierre-Marie Pédrot
2017-09-05
Quotations for auto-related tactics.
Pierre-Marie Pédrot
2017-09-04
More notations for primitive tactics.
Pierre-Marie Pédrot
2017-09-04
Implementing the non-strict mode.
Pierre-Marie Pédrot
2017-09-04
Better backtraces for a few datatypes.
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
Introducing a macro for constr matching.
Pierre-Marie Pédrot
2017-09-03
Uniform handling of locations in the various AST.
Pierre-Marie Pédrot
2017-09-02
Fix coq/ltac2#15: Ltac2 scope cannot be disabled after it is required.
Pierre-Marie Pédrot
2017-09-01
Ensuring the Ltac definitions have lowercase names.
Pierre-Marie Pédrot
2017-08-31
Fix coq/ltac2#10: Antiquotation syntax breaks when backtracking across `Requi...
Pierre-Marie Pédrot
2017-08-27
Introducing rebindable toplevel definitions.
Pierre-Marie Pédrot
2017-08-25
Introducing a distinct bindings scope.
Pierre-Marie Pédrot
2017-08-25
Renaming the bindings scope into with_bindings.
Pierre-Marie Pédrot
2017-08-25
Respect the default goal selector in toplevel invocations.
Pierre-Marie Pédrot
2017-08-24
Adding a notation scope for global references.
Pierre-Marie Pédrot
2017-08-24
Adding a scope for reduction flags.
Pierre-Marie Pédrot
2017-08-18
Exporting scopes for occurrences.
Pierre-Marie Pédrot
2017-08-11
Introducing a syntax for goal dispatch.
Pierre-Marie Pédrot
2017-08-07
Introducing grammar-free tactic notations.
Pierre-Marie Pédrot
2017-08-05
Exporting the rewrite tactic.
Pierre-Marie Pédrot
2017-08-04
Introducing quotations for the rewrite tactic.
Pierre-Marie Pédrot
2017-08-04
Introducing notations for destruct and induction arguments.
Pierre-Marie Pédrot
2017-08-02
Tentatively implementing apply.
Pierre-Marie Pédrot
2017-08-02
Extending the set of tactic scopes.
Pierre-Marie Pédrot
2017-08-01
Introducing the all-mighty intro-patterns.
Pierre-Marie Pédrot
2017-08-01
Adding new scopes for standard Ltac structures.
Pierre-Marie Pédrot
2017-07-28
Allowing generic patterns in let-bindings.
Pierre-Marie Pédrot
[next]
