index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
tac2quote.mli
Age
Commit message (
Expand
)
Author
2018-11-19
Adding a module to manipulate Ltac1 values.
Pierre-Marie Pédrot
2018-06-18
Adapt to Coq's PR #7797 (removal of reference).
Maxime Dénès
2018-06-18
Do not rely on the Ident vs. Qualid artificial separation.
Pierre-Marie Pédrot
2018-05-25
Renaming global_reference according to Coq PR #6156.
Hugo Herbelin
2018-03-10
Merge pull request coq/ltac2#46 from ejgallego/located+libnames
Pierre-Marie Pédrot
2018-03-10
[coq] Adapt to coq/coq#6831.
Emilio Jesus Gallego Arias
2018-03-05
[coq] Adapt to correct LTAC module packing coq/coq#6869
Emilio Jesus Gallego Arias
2017-10-30
Introducing the change tactic.
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-26
Adding quotations for the assert family of tactics.
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-06
Code factorization.
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-08-29
Implementing Ltac2 antiquotations in constr syntax.
Pierre-Marie Pédrot
2017-08-25
Do not return STRING scopes in the tuple produced by "seq" scopes.
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
Removing dead code.
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
Code simplification in quotations.
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
Introducing notations for destruct and induction arguments.
Pierre-Marie Pédrot
2017-08-02
Properly implementing the notation to easily access hypotheses.
Pierre-Marie Pédrot
2017-08-02
Adding the open_constr scope
Pierre-Marie Pédrot
2017-08-01
Don't reuse Coq AST for binding quotations.
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
