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
*
Fix bug #4661: Cannot mask the absolute name.
Pierre-Marie Pédrot
2016-10-01
*
Merge branch 'v8.5' into v8.6
Maxime Dénès
2016-09-30
|
\
|
*
Fix test-suite.
Maxime Dénès
2016-09-30
*
|
Ignore file names in warning emitted by test-suite/output/* (#5111)
Enrico Tassi
2016-09-30
*
|
Merge branch 'v8.5' into v8.6
Maxime Dénès
2016-09-30
|
\
|
*
|
Arguments: cleanup + detect discrepancy rename/implicit (#3753)
Enrico Tassi
2016-09-29
|
*
Fix a bug in subst releaved by an OCaml warning.
Maxime Dénès
2016-09-29
*
|
Argument : assert does fail if no arg is given (fix #4864)
Enrico Tassi
2016-09-29
*
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-09-14
|
\
|
|
*
Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.
Hugo Herbelin
2016-09-12
*
|
Merge remote-tracking branch 'github-coq/pr/249' into v8.6
Matthieu Sozeau
2016-09-12
|
\
\
|
*
|
no-refold patch
Paul Steckler
2016-09-09
*
|
|
Fix output test-suite after commit 0d3c319.
Pierre-Marie Pédrot
2016-09-09
|
/
/
*
|
Fixing output test-suite after warning for inner Requires.
Pierre-Marie Pédrot
2016-08-30
|
*
Fix Errors.out missing a dot...
Matthieu Sozeau
2016-07-19
*
|
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.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
*
|
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
[next]