aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Expand)Author
2019-12-03Printing: Interleaving search for notations and removal of coercions.Hugo Herbelin
2019-11-29Merge PR #11076: Remove all remaining calls to “omega” from the standard ...Emilio Jesus Gallego Arias
2019-11-26Merge PR #11090: Printing of coercions to which a notation is associated: a r...Emilio Jesus Gallego Arias
2019-11-25Test-suite: avoid using “omega”Vincent Laporte
2019-11-21A refined version of #8890 which prevents #11033.Hugo Herbelin
2019-11-20Combine similar arguments when printing Arguments commandGaëtan Gilbert
2019-11-11Miscellaneous improvements of the syntax of records.Hugo Herbelin
2019-11-01Add extraction for primitive floatsErik Martin-Dorel
2019-11-01Make primitive float work on WindowsPierre Roux
2019-11-01Pretty-printing primitive float constantsErik Martin-Dorel
2019-10-31Merge PR #10985: Print argument info as an Arguments command in AboutEmilio Jesus Gallego Arias
2019-10-31Merge PR #9883: Add support for Sorts in numeral notationsVincent Laporte
2019-10-31restore red behaviour printingGaëtan Gilbert
2019-10-31Fix output testsGaëtan Gilbert
2019-10-29`assert_succeeds`&`assert_fails`: multisuccess fixJason Gross
2019-10-28Add support for Sorts in numeral notationsJason Gross
2019-10-17Fix Locate printing regressionGuillaume Melquiond
2019-10-14Merge PR #10811: Allow SProp default onPierre-Marie Pédrot
2019-10-05Fix #10669 incorrect substitution in context outside sectionGaëtan Gilbert
2019-10-04Allow SProp default onGaëtan Gilbert
2019-09-16Re-implementation of zifyFrédéric Besson
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 13:07:13 +0000