index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
Commit message (
Expand
)
Author
Age
*
Merge PR #688: Binding universe constraints in Definition/Inductive/etc...
Maxime Dénès
2017-09-26
|
\
*
\
Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of ...
Maxime Dénès
2017-09-25
|
\
\
*
\
\
Merge PR #1083: Fixing bug in building _rect scheme for inductive types with ...
Maxime Dénès
2017-09-25
|
\
\
\
*
\
\
\
Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in 4...
Maxime Dénès
2017-09-25
|
\
\
\
\
*
\
\
\
\
Merge PR #1060: An optimization of tactic constructor
Maxime Dénès
2017-09-25
|
\
\
\
\
\
|
|
|
|
*
|
Fixing #5755 (discharging of inductive types not correct with let-ins).
Hugo Herbelin
2017-09-23
|
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
*
|
|
Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).
Hugo Herbelin
2017-09-23
|
|
|
*
|
Fixing _rect bug for inductive types with let-ins and non-rec uniform params.
Hugo Herbelin
2017-09-23
|
|
_
|
/
/
|
/
|
|
|
*
|
|
|
A possible fix to BZ#5750 (ability to print context of ltac subterm match).
Hugo Herbelin
2017-09-21
|
|
/
/
|
/
|
|
|
*
|
An optimization of tactic constructor.
Hugo Herbelin
2017-09-19
|
/
/
*
|
Merge PR #1050: Avoid extra failure in the "constructor" tactic (bug #5666).
Maxime Dénès
2017-09-19
|
\
\
|
|
*
Don't lose names in UState.universe_context.
Gaëtan Gilbert
2017-09-19
|
|
*
test-suite: polymorphism
Matthieu Sozeau
2017-09-19
|
|
*
Allow declaring universe binders with no constraints with @{|}
Gaëtan Gilbert
2017-09-19
|
|
*
Allow declaring universe constraints at definition level.
Matthieu Sozeau
2017-09-19
*
|
|
Merge PR #920: kernel: bugfix in filter_stack_domain.
Maxime Dénès
2017-09-19
|
\
\
\
|
|
_
|
/
|
/
|
|
|
*
|
Add test-suite script by Cyprien Mangin
Matthieu Sozeau
2017-09-18
*
|
|
Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" In...
Maxime Dénès
2017-09-15
|
\
\
\
*
\
\
\
Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" work...
Maxime Dénès
2017-09-15
|
\
\
\
\
*
\
\
\
\
Merge PR #811: Addressing #5434 (ltac pattern-matching refusing to match anon...
Maxime Dénès
2017-09-15
|
\
\
\
\
\
|
|
|
|
|
*
Avoid extra failure in the "constructor" tactic (bug #5666).
Guillaume Melquiond
2017-09-14
|
|
_
|
_
|
_
|
/
|
/
|
|
|
|
*
|
|
|
|
Fixing bug #5693 (treating empty notation format as any format).
Hugo Herbelin
2017-09-12
*
|
|
|
|
Fixing a bug of recursive notations introduced in dfdaf4de.
Hugo Herbelin
2017-09-12
*
|
|
|
|
Fixing little inaccuracy in coercions to ident or name.
Hugo Herbelin
2017-09-12
*
|
|
|
|
Merge PR #1017: Addressing BZ#5713 (classical_left/classical_right artificial...
Maxime Dénès
2017-09-11
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #997: coqdoc: Support comments in verbatim output
Maxime Dénès
2017-09-07
|
\
\
\
\
\
\
*
|
|
|
|
|
|
fix test-suite/coq-makefile/findlib-package on windows
Enrico Tassi
2017-09-04
|
|
*
|
|
|
|
Addressing BZ#5713 (classical_left/classical_right artificially restricted).
Hugo Herbelin
2017-09-03
|
|
/
/
/
/
/
|
/
|
|
|
|
|
*
|
|
|
|
|
Merge PR #996: Fix BZ#5697: Congruence does not work with primitive projections
Maxime Dénès
2017-08-31
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #995: Program: fix BZ#5683, missing lift when building case predicate
Maxime Dénès
2017-08-31
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #994: Fix BZ#5245 hnf on projections with simpl never flag
Maxime Dénès
2017-08-31
|
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
Merge PR #958: coq_makefile: build/use .cma for packed plugins too
Maxime Dénès
2017-08-31
|
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
Merge PR #998: Avoid running interactive tests on Windows.
Maxime Dénès
2017-08-30
|
\
\
\
\
\
\
\
\
\
\
|
|
|
|
|
|
|
|
|
*
|
Fixing part of #5707 (allowing destruct to use non dependent case analysis).
Hugo Herbelin
2017-08-30
|
|
*
|
|
|
|
|
|
|
|
coq_makefile(pack): ml -> cmx --pack-> cmx -> cmxa -> cmxs
Enrico Tassi
2017-08-29
|
*
|
|
|
|
|
|
|
|
|
Avoid running interactive tests on Windows.
Maxime Dénès
2017-08-29
|
|
|
|
|
*
|
|
|
|
|
Properly handling parameters of primitive projections in cctac.
Pierre-Marie Pédrot
2017-08-29
|
|
|
|
|
*
|
|
|
|
|
Fix BZ#5697: Congruence does not work with primitive projections.
Pierre-Marie Pédrot
2017-08-29
|
|
_
|
_
|
_
|
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
|
Merge PR #916: Fixing notation bug 5608 involving { } and a slight restructur...
Maxime Dénès
2017-08-29
|
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
Merge PR #830: Moving assert (the "Cut" rule) to new proof engine
Maxime Dénès
2017-08-29
|
\
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
\
Merge PR #773: [flags] Remove XML output flag.
Maxime Dénès
2017-08-29
|
\
\
\
\
\
\
\
\
\
\
\
\
|
|
_
|
_
|
/
/
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
coq_makefile: use dedicated variable for extra packages
Enrico Tassi
2017-08-29
|
|
|
|
*
|
|
|
|
|
|
|
coq_makefile: test using findlib's package
Enrico Tassi
2017-08-29
|
|
_
|
_
|
/
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
coqdoc: Support comments in verbatim output
Tej Chajed
2017-08-29
|
|
|
|
|
|
|
|
_
|
/
/
|
|
|
|
|
|
|
/
|
|
|
|
|
|
*
|
|
|
|
|
|
Adding a test for #5569 (warning about skipping spaces).
Hugo Herbelin
2017-08-29
|
|
|
*
|
|
|
|
|
|
Dropping former fix to bug #5469 (notation format not recognizing curly braces).
Hugo Herbelin
2017-08-29
|
|
|
*
|
|
|
|
|
|
A little reorganization of notations + a fix to #5608.
Hugo Herbelin
2017-08-29
|
|
|
|
|
_
|
/
/
/
/
|
|
|
|
/
|
|
|
|
|
|
|
|
|
*
|
|
|
|
primproj: fix bug 5245, hnf on proj with simpl never flag.
Matthieu Sozeau
2017-08-25
|
|
|
|
/
/
/
/
/
|
|
|
|
*
/
/
/
Program: fix BZ#5683, missing lift when building case predicate
Matthieu Sozeau
2017-08-24
|
|
|
|
/
/
/
/
|
|
|
|
|
*
/
Ensuring all .v files end with a newline to make "sed -i" work better on them.
Hugo Herbelin
2017-08-21
|
|
|
|
|
/
/
|
|
|
|
/
|
|
[next]
Maxime Dénès
Hugo Herbelin
Gaëtan Gilbert
Matthieu Sozeau
Gaëtan Gilbert
Matthieu Sozeau
Guillaume Melquiond
Enrico Tassi
Pierre-Marie Pédrot
Tej Chajed