index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
Age
Commit message (
Expand
)
Author
2019-05-24
Merge PR #10233: Fixing typos - Part 3
Théo Zimmermann
2019-05-24
Merge PR #10163: Fix dependencies of new test file and fix macOS issues.
Vincent Laporte
2019-05-23
Fixing typos - Part 3
JPR
2019-05-23
Fixing typos - Part 3
JPR
2019-05-23
do not parse `|` as infix in patterns; parse `|}` as `|` `}`
Georges Gonthier
2019-05-22
Fix dependencies of new test file.
Théo Zimmermann
2019-05-22
Fix changelog test file on macOS: do not use ls + wc.
Théo Zimmermann
2019-05-22
Merge PR #10177: Fix #10176: shadowing vs automatic class based generalizatio...
Hugo Herbelin
2019-05-22
Merge PR #10211: Use grep in changelog test instead of adhoc reads
Théo Zimmermann
2019-05-22
Use grep in changelog test instead of adhoc reads
Gaëtan Gilbert
2019-05-22
Partly revert micromega parsing using typeclasses.
Frédéric Besson
2019-05-20
Merge PR #9530: Remove `VtUnkown` classification
Gaëtan Gilbert
2019-05-20
Merge PR #9873: Remove test file with Timeout that failed spuriously.
Gaëtan Gilbert
2019-05-20
Remove VtUnknown classification
Maxime Dénès
2019-05-20
Remove Refine Instance Mode option
Maxime Dénès
2019-05-19
Implicit Quantifiers recurse in continuation of let-in
Jasper Hugunin
2019-05-16
Fix #10176: shadowing vs automatic class based generalization
Gaëtan Gilbert
2019-05-14
Merge PR #10135: Make detyping robust w.r.t. indexed anonymous variables
Pierre-Marie Pédrot
2019-05-13
Merge PR #10085: Do not include unreleased changelog in released versions.
Vincent Laporte
2019-05-13
Merge PR #10076: [Canonical structures] Annotation to field declarations to p...
Enrico Tassi
2019-05-13
Make detyping robust w.r.t. indexed anonymous variables
Maxime Dénès
2019-05-13
Merge PR #10061: Print custom grammar entries
Vincent Laporte
2019-05-10
Use Print Custom Grammar to inspect custom entries
Jasper Hugunin
2019-05-10
[Attributes] Allow explicit value for two-valued attributes
Vincent Laporte
2019-05-10
Merge PR #10058: Remove various circumvolutions from reduction behaviors
Enrico Tassi
2019-05-10
Merge PR #9854: Improve field_simplify on fractions with constant denominator
Michael Soegtrop
2019-05-10
Remove various circumvolutions from reduction behaviors
Maxime Dénès
2019-05-09
Merge PR #10046: [primitive integers] Make div21 implems consistent with its ...
Maxime Dénès
2019-05-08
Add a test that unreleased changelog of released versions is empty.
Théo Zimmermann
2019-05-07
Show diffs in error messages only if Diffs is enabled
Jim Fehrle
2019-05-07
[Test-suite] Add output case for issue #9370
Vincent Laporte
2019-05-07
Merge PR #10016: [test-suite] Remove a test with a Timeout that fails frequen...
Vincent Laporte
2019-05-07
Merge PR #10002: Integrate ltac2
Théo Zimmermann
2019-05-07
Integrate build and documentation of Ltac2
Maxime Dénès
2019-05-05
Merge PR #10059: Fixing bugs introduced in change_no_check
Pierre-Marie Pédrot
2019-05-04
Merge PR #9996: Fix #5752: `Hint Mode` ignored for type classes that appear a...
Pierre-Marie Pédrot
2019-05-03
Tactics: fixing "change_no_check in".
Hugo Herbelin
2019-05-03
[primitive integers] Make div21 implems consistent with its specification
Pierre Roux
2019-05-03
Fix #9994: `revert dependent` is extremely slow.
Pierre-Marie Pédrot
2019-05-02
Merge PR #10017: Exposing a change_no_check tactic
Pierre-Marie Pédrot
2019-05-02
Test case for #5752
Maxime Dénès
2019-04-30
Merge PR #10032: Remove leftover test suite file Quote.out
Emilio Jesus Gallego Arias
2019-04-30
Remove leftover test suite file Quote.out
Gaëtan Gilbert
2019-04-30
Merge PR #9995: fix `simpl_rel` and notations, `{pred T}` alias, `nonPropType...
Enrico Tassi
2019-04-30
Mini-test.
Hugo Herbelin
2019-04-30
Merge PR #9349: Fix #9344, #9348: incorrect unsafe to_constr in vnorm
Maxime Dénès
2019-04-30
fix `simpl_rel` and notations, `{pred T}` alias, `nonPropType` interface
Georges Gonthier
2019-04-29
Merge PR #9987: Fix #9180 by reverting #9249 and #8187
Emilio Jesus Gallego Arias
2019-04-29
Fix variant of #9344 for native_compute
Maxime Dénès
2019-04-29
Fix #9344, #9348: incorrect unsafe to_constr in vnorm
Gaëtan Gilbert
[next]