aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Expand)Author
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
2018-11-09Add a test for bug #8939.Pierre-Marie Pédrot
2018-11-02Remove is_universe_polymorphism from printingGaëtan Gilbert
2018-10-31Notations: fixing a bug with abbreviations in custom entries.Hugo Herbelin
2018-10-26Add record names to multiple records error messageTej Chajed
2018-10-26Correctly report non-projection fields in recordsTej Chajed
2018-10-10Miscellaneous refinements/cleaning of module printing.Hugo Herbelin
2018-10-09Refactoring of Micromega code using a Simplex linear solverFrédéric Besson
2018-10-08Merge PR #8630: Some cleaning in the test suiteEnrico Tassi
2018-10-04Merge PR #7361: Towards selecting "best" unification failure among severalPierre-Marie Pédrot
2018-10-04Test-suite: avoid explicit references to “Top”Vincent Laporte
2018-10-04test-suite: cleaningVincent Laporte
2018-10-04test-suite: rename a few filesVincent Laporte
2018-10-03Merge PR #8634: (For v8.9 and master) Remove -compat 8.6 and document the com...Théo Zimmermann
2018-10-02Update the -compat flagsJason Gross
2018-10-02Revert #6651: Use r.(p) syntax to print primitive projectionsMaxime Dénès
2018-09-27Inference of return clause: giving uniformly priority to "small inversion".Hugo Herbelin
2018-09-27Unification failure: don't give preference to a "beyond capabilities" error.Hugo Herbelin
2018-09-27Merge PR #8475: Centralize the reliance on abstract universe context internalsGaëtan Gilbert
2018-09-23Checking if low-level name printers are used on purpose or not.Hugo Herbelin
2018-09-21Remove hash based univ level compareGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 11:15:15 +0000