aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Expand)Author
2020-06-08Don't suggest Proof using when no section variablesGaëtan Gilbert
2020-05-25Fix output tests for location errors when running in async mode.Théo Zimmermann
2020-05-22Merge PR #11986: [primitive floats] Add low level printingPierre-Marie Pédrot
2020-05-19[primitive floats] Add low level hexadecimal printingPierre Roux
2020-05-18Merge PR #11980: Improve spacing in Print AssumptionsEmilio Jesus Gallego Arias
2020-05-18Improve spacing in Print AssumptionsGaëtan Gilbert
2020-05-17Ltac2: add notations for eval cbv in ... and other in place reductionsMichael Soegtrop
2020-05-15Test new Search features.Théo Zimmermann
2020-05-15Deprecate SearchHead.Théo Zimmermann
2020-05-15Cleaning the use of pstate and evar_map in Search.Hugo Herbelin
2020-05-15Search: Displaying the "use About" notice only when really needed.Hugo Herbelin
2020-05-15Merge PR #12323: Fixes #12322: anomaly when printing "fun" binders with impli...Emilio Jesus Gallego Arias
2020-05-15Merge PR #11948: Hexadecimal numeralsHugo Herbelin
2020-05-14Fixes #12322 (anomaly when printing "fun" binders with implicit types).Hugo Herbelin
2020-05-14Merge PR #12097: Interleave commandline require/set/unset commandsEmilio Jesus Gallego Arias
2020-05-13Extending support for mixing binders and terms in abbreviations.Hugo Herbelin
2020-05-13Test interleaving of command-line options.Théo Zimmermann
2020-05-12Merge PR #12223: Locating error again in atomic tactics (fixes #12152)Pierre-Marie Pédrot
2020-05-10Adding tests for error locationHugo Herbelin
2020-05-09Add a `with_strategy` tacticJason Gross
2020-05-09Add hexadecimal numeralsPierre Roux
2020-05-09Merge PR #12163: Fix #12159 (Numeral Notations do not play well with multiple...Hugo Herbelin
2020-05-09Merge PR #12263: HaskellExtr: Add type annotations to Prelude.==Kazuhiko Sakaguchi
2020-05-06HaskellExtr: Add type annotations to Prelude.==Jason Gross
2020-05-02Fix #12159 (Numeral Notations do not play well with multiple scopes for the s...Pierre Roux
2020-05-01Testing different combinations of non truly recursive (co)fixpoints.Hugo Herbelin
2020-04-28Merge PR #12003: Improve error messages for Set and Unset commands.Emilio Jesus Gallego Arias
2020-04-22Merge PR #11694: Support printing argument-free abbreviations in custom entri...Emilio Jesus Gallego Arias
2020-04-20Improve undeclared key messages.Théo Zimmermann
2020-04-17Merge PR #11135: Simplifying the code declaring the constants bound to primit...Pierre-Marie Pédrot
2020-04-16Merge PR #12101: Add needed commas in messageGaëtan Gilbert
2020-04-15Add needed commas in messageJim Fehrle
2020-04-15[proof] Move functions related to `Proof.t` to `Proof`Emilio Jesus Gallego Arias
2020-04-14Merge PR #11957: [stdlib] update sigma-type notationsHugo Herbelin
2020-04-14Merge PR #11820: Partial importsMaxime Dénès
2020-04-13Add specific test for "useless" syndefGaëtan Gilbert
2020-04-13Simplifying the declaration of constants bound to primitive projections.Hugo Herbelin
2020-04-11If a custom entry has global, a bound variable is valid in this entry.Hugo Herbelin
2020-04-11If a custom entry has global, an argument-free abbreviation is valid in this ...Hugo Herbelin
2020-04-06Fix #11934 equality on constrexpr ignores instances of explicit applicationsGaëtan Gilbert
2020-04-03Improve error messages for Set and Unset commands.Théo Zimmermann
2020-04-01add tests for notations with sigma typesOlivier Laurent
2020-03-31Remove special case for implicit inductive parametersMaxime Dénès
2020-03-31Merge PR #11668: Helping issue #11659 by leaving only the Cast hack in the gr...Maxime Dénès
2020-03-29Merge PR #11859: Warn when non exactly parsing non floating-pointHugo Herbelin
2020-03-27Helping issue #11659 by leaving only the Cast hack in the grammar.Hugo Herbelin
2020-03-26Print a warning when parsing non floating-point values.Pierre Roux
2020-03-25Nicer printing for decimal constants in QPierre Roux
2020-03-25Nicer printing for decimal constants in RPierre Roux
2020-03-22Testing notations which are specific numerals.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 18:25:18 +0000