aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Expand)Author
2019-09-09[stdlib] Do not put INR_eq in the “real” hint databaseVincent Laporte
2019-09-04Merge PR #10577: Fix #7348: extraction of dependent record projectionsMaxime Dénès
2019-09-04Merge PR #10612: Fix feedback levelsEmilio Jesus Gallego Arias
2019-09-02Merge PR #10648: [extraction] Fix #7191: Avoid unsound eta-reductionMaxime Dénès
2019-08-29Make sure that all query commands return a notice (not an info) feedbackMaxime Dénès
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-08-10[extraction] Fix #7191: Avoid unsound eta-reductionKazuhiko Sakaguchi
2019-08-08Fix regression of #10637 (-emacs arg sets color to `EMACS)Jim Fehrle
2019-07-31Fix #7348: extraction of dependent record projectionsKazuhiko Sakaguchi
2019-07-02Improve the ambiguous paths warning to indicate which path is ambiguous with ...Kazuhiko Sakaguchi
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-25Documenting syntax "injection ... as [= pat1 ... patn ]".Hugo Herbelin
2019-05-23Fixing typos - Part 3JPR
2019-05-22Partly revert micromega parsing using typeclasses.Frédéric Besson
2019-05-13Merge PR #10061: Print custom grammar entriesVincent Laporte
2019-05-10Use Print Custom Grammar to inspect custom entriesJasper Hugunin
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-07Show diffs in error messages only if Diffs is enabledJim Fehrle
2019-05-07[Test-suite] Add output case for issue #9370Vincent Laporte
2019-04-30Remove leftover test suite file Quote.outGaëtan Gilbert
2019-04-29Merge PR #9987: Fix #9180 by reverting #9249 and #8187Emilio Jesus Gallego Arias
2019-04-29Merge PR #9651: [ssr] Add tactics under and overCyril Cohen
2019-04-29Test-suite: add a case for issue #9180Vincent Laporte
2019-04-29Revert #8187Vincent Laporte
2019-04-29Revert #9249Vincent Laporte
2019-04-23[ssr] set under's tactic argument at LEVEL 3Erik Martin-Dorel
2019-04-23[ssr] Define over as a rewrite rule & Merge 'Under[ _ ] notationsErik Martin-Dorel
2019-04-23[ssr] Add small output test for "under eq_G => m do rewrite subnn"Erik Martin-Dorel
2019-04-23Merge PR #9889: Fix pretty-printing of primitive integersMaxime Dénès
2019-04-06Fix numeral notations test in async mode.Gaëtan Gilbert
2019-04-06Fix pretty-printing of primitive integersErik Martin-Dorel
2019-04-02Add parsing of decimal constants (e.g., 1.02e+01)Pierre Roux
2019-04-01Merge PR #9725: Lia: various impovements (support for #8764, fix #9268 and ...Vincent Laporte
2019-04-01Add test-case for #9840Jason Gross
2019-04-01Several improvements and fixes of LiaFrédéric Besson
2019-03-30Error when [foo.(bar)] is used with nonprojection [bar]Gaëtan Gilbert
2019-03-28Merge PR #9743: Relax the ambiguous path condition of coercionEnrico Tassi
2019-03-20Merge PR #8669: Show diffs in some error messagesEmilio Jesus Gallego Arias
2019-03-14Relax the ambiguous path condition of coercionKazuhiko Sakaguchi
2019-03-14Inductives in SProp, forbid primitive records with only sprop fieldsGaëtan Gilbert
2019-03-14Fix Require in output test for reals syntaxGaëtan Gilbert
2019-02-28Show diffs in error messages if color is enabledJim Fehrle
2019-02-28Implement a method for manual declaration of implicits.Jasper Hugunin
2019-02-19Notations: Fixing a printing bug with patterns.Hugo Herbelin
2019-02-18Merge PR #9142: Disable Ltac backtracesHugo Herbelin
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-02-05Unset the Ltac backtrace printing by default.Pierre-Marie Pédrot
2019-02-04Primitive integersMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 08:21:07 +0000