aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2020-05-22Merge PR #11986: [primitive floats] Add low level printingPierre-Marie Pédrot
2020-05-21Merge PR #12368: Print a newline at the end of timing tablesGaëtan Gilbert
2020-05-21Merge PR #12358: [topfmt] Set formatter + flush fixGaëtan Gilbert
2020-05-20Print a newline at the end of timing tablesJason Gross
2020-05-20Merge PR #12350: [test-suite] Ensure copies of files are writableGaëtan Gilbert
2020-05-19[topfmt] Set formatter + flush fixEmilio Jesus Gallego Arias
2020-05-19[primitive floats] Add low level hexadecimal printingPierre Roux
2020-05-18Merge PR #12289: test-suite: fix bug causing unit tests to be skippedHugo Herbelin
2020-05-18[test-suite] Ensure copies of files are writableEmilio Jesus Gallego Arias
2020-05-18Update to 8.13.Théo Zimmermann
2020-05-18Merge PR #11980: Improve spacing in Print AssumptionsEmilio Jesus Gallego Arias
2020-05-18Merge PR #12345: test-suite/Makefile: fix incomplete prerequisite listEmilio Jesus Gallego Arias
2020-05-18test-suite/Makefile: fix incomplete prerequisite listGaëtan Gilbert
2020-05-18Improve spacing in Print AssumptionsGaëtan Gilbert
2020-05-17Revert "[test] unit tests for ide/coq_lex.ml" + makefile supportGaëtan Gilbert
2020-05-17Fix proof_diffs_test.mlGaëtan Gilbert
2020-05-17test-suite: fix bug causing unit tests to be skippedGaëtan Gilbert
2020-05-17Ltac2: add notations for eval cbv in ... and other in place reductionsMichael Soegtrop
2020-05-16Merge PR #12326: Fix #11761: Functional Induction throws unrecoverable error.Emilio Jesus Gallego Arias
2020-05-16Fix #11761: Functional Induction throws unrecoverable error.Pierre Courtieu
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-15Merge PR #11992: do not re-export ListNotations from ProgramAnton Trunov
2020-05-14Merge PR #12256: Move the static check of evaluability in unfold tactic to ru...Hugo Herbelin
2020-05-14Add test for #11727, which was indirectly fixed by this PR.Pierre-Marie Pédrot
2020-05-14Move the static check of evaluability in unfold tactic to runtime.Pierre-Marie Pédrot
2020-05-14Fixes #12234 (wrong environment for Show Proof).Hugo 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-14Merge PR #8808: Extending support for mixing binders and terms in abbreviationsEmilio Jesus Gallego Arias
2020-05-14Merge PR #12315: Tests for bugs #9583 (fixed by #11613) and #9679.Emilio Jesus Gallego Arias
2020-05-13Extending support for mixing binders and terms in abbreviations.Hugo Herbelin
2020-05-13Tests for bugs #9583 (fixed by #11613) and #9679.Hugo Herbelin
2020-05-13Merge PR #11828: [obligations] Deprecated flag cleanupGaëtan Gilbert
2020-05-13Test interleaving of command-line options.Théo Zimmermann
2020-05-12Merge PR #11503: Allow to rebind the old value of a mutable Ltac2 entry.Jason Gross
2020-05-12Merge PR #12223: Locating error again in atomic tactics (fixes #12152)Pierre-Marie Pédrot
2020-05-12Merge PR #12146: Fixes #10812: tactic subst failure with section variables in...Pierre-Marie Pédrot
2020-05-11More tests of rebinding Ltac2 definitionsKenji Maillard
2020-05-11Merge PR #12254: In non-strict mode, accept any variable as a tactic reference.Hugo Herbelin
2020-05-11Correcting ltac2's documentation on values turning test into proper check.Kenji Maillard
2020-05-11Allow to rebind the old value of a mutable Ltac2 entry.Pierre-Marie Pédrot
2020-05-10Adding tests for error locationHugo Herbelin
2020-05-09Revert "[with_strategy] Fix for coqchk"Jason Gross
2020-05-09Fix a bug with with_strategy, behavior on multisuccess tacticsJason Gross
2020-05-09Elaborate with_strategy warningJason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 13:15:17 +0000