aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
2020-07-01UIP in SPropGaëtan Gilbert
2020-06-29[test-suite] async-proofs off in tests with Fail TimeoutEnrico Tassi
2020-05-18Update to 8.13.Théo Zimmermann
2020-05-16Fix #11761: Functional Induction throws unrecoverable error.Pierre Courtieu
2020-05-15Merge PR #11992: do not re-export ListNotations from ProgramAnton Trunov
2020-05-14Move the static check of evaluability in unfold tactic to runtime.Pierre-Marie Pédrot
2020-05-13Merge PR #11828: [obligations] Deprecated flag cleanupGaëtan Gilbert
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-08In non-strict mode, accept any variable as a tactic reference.Pierre-Marie Pédrot
2020-05-02LtacProf now handles multi-success backtrackingJason Gross
2020-04-30do not re-export ListNotations from Program: fix testsuiteAntonio Nikishaev
2020-04-28Stop relying on side-effects for recursive scheme declaration.Pierre-Marie Pédrot
2020-04-13Partial import inductive(..)Gaëtan Gilbert
2020-04-13test partial importGaëtan Gilbert
2020-04-10[obligations] Deprecated flag cleanupEmilio Jesus Gallego Arias
2020-04-07Support universe bindings and universe constraints in Let definitions.Théo Zimmermann
2020-03-31Include review suggestionsGaëtan Gilbert
2020-03-31Remove special case for implicit inductive parametersMaxime Dénès
2020-03-31Merge PR #11684: Remove spurious anomalies in kernel reductionPierre-Marie Pédrot
2020-03-28Remove SearchAbout command, deprecated in 8.5Jim Fehrle
2020-03-19Interpret the Export modifier of Set and Unset as an attribute.Théo Zimmermann
2020-03-19Remove spurious anomalies in kernel reductionGaëtan Gilbert
2020-03-18Merge PR #11559: Remove year in headers.Hugo Herbelin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-18Export the user-facing attribute for hint locality.Pierre-Marie Pédrot
2020-03-13Implementing postponed constraints in TC resolutionMatthieu Sozeau
2020-03-03Adding an alias "pose proof (x:=a)" for "pose proof a as x".Hugo Herbelin
2020-02-25Fixing residual bug of #11120.Hugo Herbelin
2020-02-24Merge PR #11588: test for x[i] notation not breaking Ltac parsingGaëtan Gilbert
2020-02-22Inherit scopes and implicit sign. in notations for partially applied pattern.Hugo Herbelin
2020-02-22Inherit argument scopes in notations to expressions of the form @f.Hugo Herbelin
2020-02-22Propagate implicit arguments in all notations for partial applications.Hugo Herbelin
2020-02-22Fixing a bug introduced in PR #10832 (new format specific to a given notation).Hugo Herbelin
2020-02-17New syntax [Inductive Acc A R | x : Prop := ...]Gaëtan Gilbert
2020-02-17Revert "Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)"Gaëtan Gilbert
2020-02-14test for x[i] notation not breaking Ltac parsingAndres Erbsen
2020-02-14Merge PR #11584: Add #[uniform] and #[nonuniform] (for Uniform Inductive Para...Maxime Dénès
2020-02-13Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)Gaëtan Gilbert
2020-02-13Arguments: removing the restriction to set an anonymous parameter implicit.Hugo Herbelin
2020-02-11Merge PR #11235: Add syntax for non maximal implicit argumentsHugo Herbelin
2020-02-08Remove -compat 8.9.Théo Zimmermann
2020-02-04Correct bug in non max local implicit argumentsSimonBoulier
2020-02-04Add syntax for non maximally inserted implicit argumentsSimonBoulier
2020-01-29Merge PR #11472: Fix #11467 ('e' was not displayed when printing decimal nota...Pierre-Marie Pédrot
2020-01-28Fix #11467Pierre Roux
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 16:33:43 +0000