aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Expand)Author
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
2018-09-21Add test for univ names of polymorphic inductives in sections.Gaëtan Gilbert
2018-09-21Universe binders are Id, not Name. Never print Var.Gaëtan Gilbert
2018-09-21Best-effort hack to provide a meaningful name for anonymous bound universes.Pierre-Marie Pédrot
2018-09-21Removing calls to AUContext.instance.Pierre-Marie Pédrot
2018-09-14Fixing yet a source of dependency on alphabetic order in unification.Hugo Herbelin
2018-09-12Remove quote pluginMaxime Dénès
2018-09-11Merge PR #7288: Isolating ltac naming out of pretyping + fixing renamingPierre-Marie Pédrot
2018-09-11Merge PR #7135: Introducing an explicit `Declare Scope` commandEmilio Jesus Gallego Arias
2018-09-10Merge PR #8417: Fixing #8416: Print Assumptions missing module information fr...Matthieu Sozeau
2018-09-10Adapting standard library to the introduction of "Declare Scope".Hugo Herbelin
2018-09-10Fixing an inconsistency in interpreting Ltac names linking to binder names.Hugo Herbelin
2018-09-05Fixing #8416 (Print Assumptions missing module information from compiled files).Hugo Herbelin
2018-08-28Close #8091: print universe context for Eval when option on.Gaëtan Gilbert
2018-08-28Fix #8291: print universe names in universe context for Check.Gaëtan Gilbert
2018-07-29Adding support for custom entries in notations.Hugo Herbelin
2018-07-26Add information to option type errorsTej Chajed
2018-07-26Merge PR #7786: In "redundant clause" pattern-matching error, show also the p...Pierre-Marie Pédrot
2018-07-25In "redundant clause" pattern-matching error, show also the pattern (#7777).Hugo Herbelin
2018-07-24Fixes #8126 (issue with notations and nested applications).Hugo Herbelin
2018-07-17Change QuestionMark for better record field missing error message.Siddharth Bhat
2018-07-12Tactic deprecation machineryMaxime Dénès
2018-06-29Workaround to fix #7731 (printing not splitting line at break hint).Hugo Herbelin
2018-06-14Merge PR #7193: Fixes #7192: Print Assumptions does not enter implementation ...Pierre-Marie Pédrot
2018-06-10Tweak printing boxes for unicode bindersRalf Jung
2018-05-25An attempt to clarify error message for Arguments needing "rename" flag.Hugo Herbelin
2018-05-17Introduce an option to allow nested lemma, and turn it off by default.Théo Zimmermann
2018-05-15[ssr] import ssreflect test suite from math-compEnrico Tassi
2018-05-13Fixing a bug in printing the body of a located notation.Hugo Herbelin
2018-05-02Making explicit that errors happen in one of five executation phases.Hugo Herbelin
2018-04-09Merge PR #7116: Fixes #7110: missing test on the absence of a "as" while look...Emilio Jesus Gallego Arias
2018-04-09Merge PR #7165: [ssr] check cleared hyps do exist (fix #7050)Maxime Dénès
2018-04-07Fixes #7192 (Print Assumptions does not enter implementation of submodules).Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-03 01:27:38 +0000