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
Commit message (
Expand
)
Author
Age
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-07-20
|
\
|
*
Some extra fixes in printing patterns in binders.
Hugo Herbelin
2016-07-19
|
*
Taking into account binding patterns when agglutinating sequences of binders.
Hugo Herbelin
2016-07-19
|
*
Fixing missing parentheses in printing of patterns in binders.
Hugo Herbelin
2016-07-19
|
*
Notations: fixing multiple binders used as terms in reverse order.
Hugo Herbelin
2016-07-19
|
*
Removing a source of clash with multiple recursive patterns in notations.
Hugo Herbelin
2016-07-19
|
*
A new step on using alpha-conversion in printing notations.
Hugo Herbelin
2016-07-18
|
*
Partial fix to #4592 (notation requiring alpha-conversion for printing).
Hugo Herbelin
2016-07-17
|
*
More examples of recursive notations, with emphasis in reference manual.
Hugo Herbelin
2016-07-17
|
*
Fixing a bug in recognizing a recursive pattern of notations
Hugo Herbelin
2016-07-17
|
*
Fixing interpretation of notations w/ opposite instances of a recursive pattern.
Hugo Herbelin
2016-07-17
|
*
Fixing printing of notations with several instances of a recursive pattern.
Hugo Herbelin
2016-07-17
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-07-13
|
\
|
|
*
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-07-13
|
|
\
|
|
*
Fixing printing of evar name in an error message of instantiate.
Hugo Herbelin
2016-07-13
*
|
|
A short test on printing evars in Show Proof (this was wrong at some time).
Hugo Herbelin
2016-07-12
|
/
/
*
|
Fix issues in test-suite revealed by warnings.
Maxime Dénès
2016-06-29
*
|
Adding a test-suite for the only printing flag.
Pierre-Marie Pédrot
2016-06-28
*
|
Patterns in binders: printing tests
Arnaud Spiwack
2016-06-27
*
|
Adding ability to put any pattern in binders, prefixed by a quote.
Daniel de Rauglaudre
2016-06-27
*
|
Fixing #4854 (regression introduced in 4d25b224 in relation with #4592).
Hugo Herbelin
2016-06-24
*
|
Exporting a generic argument induction_arg. As a consequence,
Hugo Herbelin
2016-06-18
*
|
proof mode: print unification constraints
Matthieu Sozeau
2016-06-16
*
|
Not taking arguments given by name or position into account when
Hugo Herbelin
2016-06-16
*
|
About printing of traces of failures while calling ltac code.
Hugo Herbelin
2016-06-06
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-04
|
\
|
|
*
Fixing subst.out after changing spacing in goal output (24a125b77).
Hugo Herbelin
2016-05-04
|
*
In Regular Subst Tactic mode, ensure that the order of hypotheses is
Hugo Herbelin
2016-05-03
|
*
Remove extraneous space in coqtop/pg output (bug #4675).
Guillaume Melquiond
2016-05-03
*
|
Revert "A heuristic to add parentheses in the presence of rules such as"
Hugo Herbelin
2016-04-27
*
|
A heuristic to add parentheses in the presence of rules such as
Hugo Herbelin
2016-04-27
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-04-24
|
\
|
|
*
Fixing output test Notations2.
Hugo Herbelin
2016-04-22
|
*
Fixing #4677 (collision of a global variable and of a local variable
Hugo Herbelin
2016-04-19
*
|
A small test of Print Ltac.
Hugo Herbelin
2016-04-09
*
|
Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...
Matthieu Sozeau
2016-04-04
|
\
\
*
\
\
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-02-13
|
\
\
\
|
|
|
/
|
|
/
|
|
*
|
Do not give a name to anonymous evars anymore. See bug #4547.
Pierre-Marie Pédrot
2016-02-13
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-17
|
\
|
|
|
*
|
Fix test suite after change in extraction.
Maxime Dénès
2015-12-15
*
|
|
Using x in output test-suite Cases.v (cosmetic).
Hugo Herbelin
2015-12-05
*
|
|
Fixing output test Cases.v.
Pierre-Marie Pédrot
2015-11-15
*
|
|
Updating test-suite after Bracketing Last Introduction Pattern set by
Hugo Herbelin
2015-11-10
*
|
|
Merge origin/v8.5 into trunk
Hugo Herbelin
2015-11-10
|
\
|
|
*
|
|
Adapting output test inference.v after c23f0cab6 (experimenting
Hugo Herbelin
2015-11-08
|
*
|
Fixing output test Existentials.v after eec77191b.
Hugo Herbelin
2015-11-07
|
/
/
*
|
Fixing a bug in reporting ill-formed inductive.
Hugo Herbelin
2015-10-22
*
|
Fixing test-suite
Hugo Herbelin
2015-10-11
*
|
Fixing untimely unexpected warning "Collision between bound variables" (#4317).
Hugo Herbelin
2015-10-11
*
|
Refining 0c320e79ba30 in fixing interpretation of constr under binders
Hugo Herbelin
2015-10-11
[next]