index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
/
output
/
ltac.out
Commit message (
Expand
)
Author
Age
*
Printing again "intros **" as "intros" by default.
Hugo Herbelin
2017-11-24
*
Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).
Hugo Herbelin
2017-11-24
*
Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).
Hugo Herbelin
2017-11-20
*
[pp] Make feedback the only logging mechanism.
Emilio Jesus Gallego Arias
2017-03-21
*
Merge remote-tracking branch 'github/pr/319' into v8.6
Maxime Dénès
2016-10-28
|
\
*
|
Adding a test for #4398 (interpretation scopes for "match goal").
Hugo Herbelin
2016-10-24
*
|
Merge branch 'v8.5' into v8.6
Hugo Herbelin
2016-10-22
|
\
\
|
*
|
Fixing printing of generic arguments of tag "var".
Hugo Herbelin
2016-10-22
|
|
*
[pp] Try to properly tag error messages in cError.
Emilio Jesus Gallego Arias
2016-10-18
|
|
/
|
/
|
*
|
Fix output test-suite after commit 0d3c319.
Pierre-Marie Pédrot
2016-09-09
*
|
Exporting a generic argument induction_arg. As a consequence,
Hugo Herbelin
2016-06-18
*
|
About printing of traces of failures while calling ltac code.
Hugo Herbelin
2016-06-06
*
|
A small test of Print Ltac.
Hugo Herbelin
2016-04-09
|
/
*
Refining 0c320e79ba30 in fixing interpretation of constr under binders
Hugo Herbelin
2015-10-11