index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
g_ltac2.ml4
Age
Commit message (
Expand
)
Author
2017-12-26
adapt to API.mli removal
Enrico Tassi
2017-11-21
[coq] Adapt to Coq's new functional EXTEND API.
Emilio Jesus Gallego Arias
2017-11-02
Factorizing entries for patterns with type constraints.
Pierre-Marie Pédrot
2017-11-02
Moving pattern type constraints to pattern AST.
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-09-26
Adding quotations for the assert family of tactics.
Pierre-Marie Pédrot
2017-09-26
Small language of combinators for lookaheads in parsing.
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-08
Using a dedicated argument for tactic quotations.
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-03
Introducing a macro for constr matching.
Pierre-Marie Pédrot
2017-09-03
Moving generic arguments to Tac2quote.
Pierre-Marie Pédrot
2017-09-03
Uniform handling of locations in the various AST.
Pierre-Marie Pédrot
2017-08-31
Fix coq/ltac2#10: Antiquotation syntax breaks when backtracking across `Requi...
Pierre-Marie Pédrot
2017-08-29
Rolling our own generic arguments.
Pierre-Marie Pédrot
2017-08-29
Implementing Ltac2 antiquotations in constr syntax.
Pierre-Marie Pédrot
2017-08-27
Introducing rebindable toplevel definitions.
Pierre-Marie Pédrot
2017-08-26
Allowing to insert calls to Ltac1 references in Ltac2.
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
Parse specifically idents as destruction arguments.
Pierre-Marie Pédrot
2017-08-25
Lookahead to cheat the constr parser in order to parse "& IDENT".
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-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-24
Introducing a quotation for global references.
Pierre-Marie Pédrot
2017-08-18
More precise type for quotation entries.
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-08
Another batch of primitive operations.
Pierre-Marie Pédrot
2017-08-08
Code simplification in quotations.
Pierre-Marie Pédrot
2017-08-07
Fix parsing of parenthesized expressions.
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
Adding locations to quotation types.
Pierre-Marie Pédrot
2017-08-04
More precise type for quoted structures.
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
Properly implementing the notation to easily access hypotheses.
Pierre-Marie Pédrot
2017-08-02
Properly classifying Ltac2 notations.
Pierre-Marie Pédrot
2017-08-02
Fixing parsing of match branches.
Pierre-Marie Pédrot
2017-08-02
Bindings use open constr quotations.
Pierre-Marie Pédrot
2017-08-02
Tentatively fixing a few parsing issues.
Pierre-Marie Pédrot
2017-08-01
Don't reuse Coq AST for binding quotations.
Pierre-Marie Pédrot
[next]
