aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Expand)Author
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
2019-01-30[toplevel] Deprecate the `-compile` flag in favor of `coqc`.Emilio Jesus Gallego Arias
2019-01-25Notations: Removing useless parentheses on abbrevs for prefix of an application.Hugo Herbelin
2019-01-09Stop [Print] from saying [is (not) universe polymorphic].Gaëtan Gilbert
2019-01-06Reworking error message for unresolved evar subterm of another evar.Hugo Herbelin
2018-12-25Fixing printing bug due to using equality ill-checking hash key of kernel name.Hugo Herbelin
2018-12-21Merge PR #9182: Stop printing Monomorphic/Polymorphic in Print.Maxime Dénès
2018-12-19Put #[universes(template)] in outputs testsGaëtan Gilbert
2018-12-17Stop printing Monomorphic/Polymorphic in Print.Gaëtan Gilbert
2018-12-12Accept argument names for extra arguments with "extra scopes"Maxime Dénès
2018-12-12Merge PR #8965: Add `String Notation` vernacular like `Numeral Notation`Hugo Herbelin
2018-12-08Do so that an error message follows the "Error:" header on the same line.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 23:45:16 +0000