aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2020-05-12Merge PR #12146: Fixes #10812: tactic subst failure with section variables in...Pierre-Marie Pédrot
2020-05-11Merge PR #12254: In non-strict mode, accept any variable as a tactic reference.Hugo 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
2020-05-09Fix the `with_strategy` tactic to work with `abstract`Jason Gross
2020-05-09Add a `with_strategy` tacticJason Gross
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-08In non-strict mode, accept any variable as a tactic reference.Pierre-Marie Pédrot
2020-05-08Merge PR #12121: Fixes #11903 and warns about non truly-recursive (co)fixpointsPierre-Marie Pédrot
2020-05-07Tactic subst now inactive on section variables occurring indirectly in goal.Hugo Herbelin
2020-05-06HaskellExtr: Add type annotations to Prelude.==Jason Gross
2020-05-05Merge PR #12227: Spring cleaning of the tactic compatibility layerEnrico Tassi
2020-05-03Add tests uncovered during bug chasing in the CI.Pierre-Marie Pédrot
2020-05-02Fix #12159 (Numeral Notations do not play well with multiple scopes for the s...Pierre Roux
2020-05-02LtacProf now handles multi-success backtrackingJason Gross
2020-05-01Testing different combinations of non truly recursive (co)fixpoints.Hugo Herbelin
2020-05-01Merge PR #12221: Replace QSeqEquiv by QCauchySeq, simplify proofs.Michael Soegtrop
2020-04-30Replace QSeqEquiv by QCauchySeq, simplify proofs.Vincent Semeria
2020-04-30[zify] add support for Nat.le, Nat.lt and Nat.eqFrédéric Besson
2020-04-29Merge PR #11606: [tools] Add memory stats to tables by defaultEmilio Jesus Gallego Arias
2020-04-29Merge PR #12027: Fix #3415: coqdoc links projections rather than constructor ...Emilio Jesus Gallego Arias
2020-04-28Stop relying on side-effects for recursive scheme declaration.Pierre-Marie Pédrot
2020-04-28Merge PR #12003: Improve error messages for Set and Unset commands.Emilio Jesus Gallego Arias
2020-04-27Merge PR #12073: Split off Nsatz tactic part into Nsatz_tacticPierre-Marie Pédrot
2020-04-27Merge PR #12175: Calculation speed of Cauchy realsMichael Soegtrop
2020-04-26constructive square rootVincent Semeria
2020-04-24Make the nsatz test-suite passJason Gross
2020-04-24Add memory stats to tables by defaultJason Gross
2020-04-24Split off Nsatz tactic part into NsatzTacticJason Gross
2020-04-22Merge PR #12023: Adding a Declare ML Module in empty file Ltac.vEmilio Jesus Gallego Arias
2020-04-22Merge PR #11694: Support printing argument-free abbreviations in custom entri...Emilio Jesus Gallego Arias
2020-04-21Adapt test-suite to #12023.Hugo Herbelin
2020-04-21Fixing #3451: coqdoc links for projections of tuples rather than for construc...Hugo Herbelin
2020-04-21Merge PR #12082: Fixes #11808: support for test-suite in -byte-only modeGaëtan Gilbert
2020-04-21Merge PR #12116: Fixing #12045: missing normalization in conclusion of custom...Pierre-Marie Pédrot
2020-04-21Merge PR #11883: Fix #7812: autounfold's behavior depends on file namesHugo Herbelin
2020-04-20Merge PR #12038: Improve undeclared goption key messages.Gaëtan Gilbert
2020-04-20Merge PR #12126: TIMEFMT: Display the output file nameGaëtan Gilbert
2020-04-20Granting coqdoc wish #7093 (definitions link to themselves).Hugo Herbelin
2020-04-20TIMEFMT: Display the output file nameJason Gross
2020-04-20Improve undeclared key messages.Théo Zimmermann
2020-04-20Fixing #12045 (missing normalization in conclusion of custom induction scheme).Hugo Herbelin
2020-04-19Fix Makefile warning: undefined variable '*'Jason Gross
2020-04-19Merge PR #12033: Let coqdoc be informed by coq about binding variables (incid...Lysxia
2020-04-17ZArith: move lia hints to a dedicated moduleVincent Laporte
2020-04-17Merge PR #11135: Simplifying the code declaring the constants bound to primit...Pierre-Marie Pédrot
2020-04-17Merge PR #11972: Fix require in sectionPierre-Marie Pédrot
2020-04-16Merge PR #12070: Ignore -native-compiler option when disabledPierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-21 05:48:23 +0000