aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2019-05-24Merge PR #10233: Fixing typos - Part 3Théo Zimmermann
2019-05-24Merge PR #10163: Fix dependencies of new test file and fix macOS issues.Vincent Laporte
2019-05-23Fixing typos - Part 3JPR
2019-05-23Fixing typos - Part 3JPR
2019-05-23do not parse `|` as infix in patterns; parse `|}` as `|` `}`Georges Gonthier
2019-05-22Fix dependencies of new test file.Théo Zimmermann
2019-05-22Fix changelog test file on macOS: do not use ls + wc.Théo Zimmermann
2019-05-22Merge PR #10177: Fix #10176: shadowing vs automatic class based generalizatio...Hugo Herbelin
2019-05-22Merge PR #10211: Use grep in changelog test instead of adhoc readsThéo Zimmermann
2019-05-22Use grep in changelog test instead of adhoc readsGaëtan Gilbert
2019-05-22Partly revert micromega parsing using typeclasses.Frédéric Besson
2019-05-20Merge PR #9530: Remove `VtUnkown` classificationGaëtan Gilbert
2019-05-20Merge PR #9873: Remove test file with Timeout that failed spuriously.Gaëtan Gilbert
2019-05-20Remove VtUnknown classificationMaxime Dénès
2019-05-20Remove Refine Instance Mode optionMaxime Dénès
2019-05-19Implicit Quantifiers recurse in continuation of let-inJasper Hugunin
2019-05-16Fix #10176: shadowing vs automatic class based generalizationGaëtan Gilbert
2019-05-14Merge PR #10135: Make detyping robust w.r.t. indexed anonymous variablesPierre-Marie Pédrot
2019-05-13Merge PR #10085: Do not include unreleased changelog in released versions.Vincent Laporte
2019-05-13Merge PR #10076: [Canonical structures] Annotation to field declarations to p...Enrico Tassi
2019-05-13Make detyping robust w.r.t. indexed anonymous variablesMaxime Dénès
2019-05-13Merge PR #10061: Print custom grammar entriesVincent Laporte
2019-05-10Use Print Custom Grammar to inspect custom entriesJasper Hugunin
2019-05-10[Attributes] Allow explicit value for two-valued attributesVincent Laporte
2019-05-10Merge PR #10058: Remove various circumvolutions from reduction behaviorsEnrico Tassi
2019-05-10Merge PR #9854: Improve field_simplify on fractions with constant denominatorMichael Soegtrop
2019-05-10Remove various circumvolutions from reduction behaviorsMaxime Dénès
2019-05-09Merge PR #10046: [primitive integers] Make div21 implems consistent with its ...Maxime Dénès
2019-05-08Add a test that unreleased changelog of released versions is empty.Théo Zimmermann
2019-05-07Show diffs in error messages only if Diffs is enabledJim Fehrle
2019-05-07[Test-suite] Add output case for issue #9370Vincent Laporte
2019-05-07Merge PR #10016: [test-suite] Remove a test with a Timeout that fails frequen...Vincent Laporte
2019-05-07Merge PR #10002: Integrate ltac2Théo Zimmermann
2019-05-07Integrate build and documentation of Ltac2Maxime Dénès
2019-05-05Merge PR #10059: Fixing bugs introduced in change_no_checkPierre-Marie Pédrot
2019-05-04Merge PR #9996: Fix #5752: `Hint Mode` ignored for type classes that appear a...Pierre-Marie Pédrot
2019-05-03Tactics: fixing "change_no_check in".Hugo Herbelin
2019-05-03[primitive integers] Make div21 implems consistent with its specificationPierre Roux
2019-05-03Fix #9994: `revert dependent` is extremely slow.Pierre-Marie Pédrot
2019-05-02Merge PR #10017: Exposing a change_no_check tacticPierre-Marie Pédrot
2019-05-02Test case for #5752Maxime Dénès
2019-04-30Merge PR #10032: Remove leftover test suite file Quote.outEmilio Jesus Gallego Arias
2019-04-30Remove leftover test suite file Quote.outGaëtan Gilbert
2019-04-30Merge PR #9995: fix `simpl_rel` and notations, `{pred T}` alias, `nonPropType...Enrico Tassi
2019-04-30Mini-test.Hugo Herbelin
2019-04-30Merge PR #9349: Fix #9344, #9348: incorrect unsafe to_constr in vnormMaxime Dénès
2019-04-30fix `simpl_rel` and notations, `{pred T}` alias, `nonPropType` interfaceGeorges Gonthier
2019-04-29Merge PR #9987: Fix #9180 by reverting #9249 and #8187Emilio Jesus Gallego Arias
2019-04-29Fix variant of #9344 for native_computeMaxime Dénès
2019-04-29Fix #9344, #9348: incorrect unsafe to_constr in vnormGaëtan Gilbert