aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Expand)Author
2020-06-25Generate names for anonymous polymorphic universesGaëtan Gilbert
2020-06-22Merge PR #12434: Slight improvement in naming dependent existential variables...Gaëtan Gilbert
2020-06-11Merge PR #12443: Fix #12442: Confusing error message when the intro pattern o...Pierre-Marie Pédrot
2020-06-11Merge PR #12423: Remove info tactic, deprecated in 8.5Pierre-Marie Pédrot
2020-06-09Merge PR #12186: CReal: changed epsilon for modulus of convergence from 1/n t...Vincent Semeria
2020-06-09CReal: changed epsilon for modulus of convergence from 1/n to 2^zMichael Soegtrop
2020-06-08Don't suggest Proof using when no section variablesGaëtan Gilbert
2020-06-06Fix #12442: Confusing error message when the intro pattern of "apply in" failsAttila Gáspár
2020-06-01Slight improvement in naming existential variables.Hugo Herbelin
2020-05-30Remove info tactic, deprecated in 8.5Jim Fehrle
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:56:22 +0000