aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Expand)Author
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
2018-12-04Giving to type_scope a softer role in printing.Hugo Herbelin
2018-12-04Printing priority to most recent notation in case of non-open scopes with delim.Hugo Herbelin
2018-12-04Using scope for printing: more tests.Hugo Herbelin
2018-12-04Fixing #8551 (missing delimiters when notation exists both lonely and in scope).Hugo Herbelin
2018-12-04Addressing issues with PR#873: performance and use of abbreviation for printing.Hugo Herbelin
2018-12-04Selecting which notation to print based on current stack of scope.Hugo Herbelin
2018-12-04Pre-isolating a notation test to avoid interferences.Hugo Herbelin
2018-11-28Add a couple more printing tests for byte/asciiJason Gross
2018-11-28Byte.v: use right-associative tuples in bitsJason Gross
2018-11-28Speed up ByteJason Gross
2018-11-28Add `String Notation` vernacular like `Numeral Notation`Jason Gross
2018-11-20Notations: Trying using a notation with or w/o removal of coercions.Hugo Herbelin
2018-11-19Merge PR #8894: Print full binders in subtyping incompatible polymorphism error.Pierre-Marie Pédrot
2018-11-16Print Universes SubgraphGaëtan Gilbert
2018-11-16We improve a little bit in printing universe constraints signature mismatch.Hugo Herbelin
2018-11-13Merge PR #8760: Automatically generate names for universes.Pierre-Marie Pédrot
2018-11-12Automatically generate names for universes.Gaëtan Gilbert
2018-11-12Don't declare universe binders for variables.Gaëtan Gilbert
2018-11-09Fix -top for univbinders output test.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 15:27:52 +0000