index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
doc
Age
Commit message (
Expand
)
Author
2018-10-23
Merge remote-tracking branch 'origin/pr/70'
Pierre-Marie Pédrot
2018-08-07
fix three small typos
Langston Barrett
2018-08-07
doc/ltac2.md: add table of contents
Langston Barrett
2018-03-13
Fix another typo in the documentation's grammar for open variants
Armael
2018-03-13
Fix a typo
Armael
2017-10-27
Adding documentation
Pierre-Marie Pédrot
2017-10-27
Adding a command to evaluate Ltac2 expressions.
Pierre-Marie Pédrot
2017-09-04
Implementing the non-strict mode.
Pierre-Marie Pédrot
2017-09-04
Quick-and-dirty backtrace mechanism for the interpreter.
Pierre-Marie Pédrot
2017-08-28
typos
gallais
2017-08-27
Introducing rebindable toplevel definitions.
Pierre-Marie Pédrot
2017-08-26
Allowing calls to Ltac2 inside Ltac1.
Pierre-Marie Pédrot
2017-08-26
Typos
Hugo Herbelin
2017-08-26
Allowing to insert calls to Ltac1 references in Ltac2.
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
Documentation about the transition from Ltac1.
Pierre-Marie Pédrot
2017-08-24
Introducing a quotation for global references.
Pierre-Marie Pédrot
2017-08-07
Introducing grammar-free tactic notations.
Pierre-Marie Pédrot
2017-08-02
Typo in documentation.
Pierre-Marie Pédrot
2017-08-02
Expanding documentation.
Pierre-Marie Pédrot
2017-08-02
Properly implementing the notation to easily access hypotheses.
Pierre-Marie Pédrot
2017-08-02
Extending the set of tactic scopes.
Pierre-Marie Pédrot
2017-08-01
Fix documentation.
Pierre-Marie Pédrot
2017-08-01
More in documentation.
Pierre-Marie Pédrot
2017-08-01
Fixup doc
Pierre-Marie Pédrot
2017-08-01
Fixup doc
Pierre-Marie Pédrot
2017-08-01
Adding documentation from the CEP.
Pierre-Marie Pédrot