aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2019-01-09Make it possible to pass flags to coq when running test suiteMaxime Dénès
2019-01-08Fix #9272: `Unset Nested Proofs Allowed` does not capture nested `Instance` p...Maxime Dénès
2019-01-08Merge PR #9292: Fixing some wrong scopes of variables in the interpretation o...Emilio Jesus Gallego Arias
2019-01-07Merge PR #9241: Fix #9240: Register for IDProp causes anomaly when non constantEnrico Tassi
2019-01-06Reworking error message for unresolved evar subterm of another evar.Hugo Herbelin
2019-01-04Handle local definitions in implicit arguments of InstanceJasper Hugunin
2018-12-30Fixing an interpretation bug of the "in" clause of "match".Hugo Herbelin
2018-12-30Do not take universes into account in lia reification.Pierre-Marie Pédrot
2018-12-26Merge PR #8734: Make diffs work for more input stringsHugo Herbelin
2018-12-25Fixing printing bug due to using equality ill-checking hash key of kernel name.Hugo Herbelin
2018-12-22Merge PR #9248: Fix #7904: update proofview env after ltac constr:()Pierre-Marie Pédrot
2018-12-21Fix #9240: Register for IDProp causes anomaly when non constantGaëtan Gilbert
2018-12-21Do not exclude "opened" bugs from reportMaxime Dénès
2018-12-21Merge PR #9182: Stop printing Monomorphic/Polymorphic in Print.Maxime Dénès
2018-12-20Make diffs work for more input stringsJim Fehrle
2018-12-20Merge PR #8488: Warning when using automatic template polymorphismPierre-Marie Pédrot
2018-12-20Merge PR #9200: [ssr] make `>` stand aloneMaxime Dénès
2018-12-19Fix #7904: update proofview env after ltac constr:()Gaëtan Gilbert
2018-12-19Put #[universes(template)] in outputs testsGaëtan Gilbert
2018-12-19Merge PR #9231: Fixes #9229: Infix not robust wrt choice of variable names in...Pierre-Marie Pédrot
2018-12-19coqchk: fix check for kelim with functorsGaëtan Gilbert
2018-12-18Merge PR #9223: Fix universe restriction in delayed mode.Pierre-Marie Pédrot
2018-12-18[ssr] make > a stand alone intro patternEnrico Tassi
2018-12-18Fixes #9229 (Infix not robust wrt choice of variable names).Hugo Herbelin
2018-12-18[ssr] new test by Arthur CharguéraudEnrico Tassi
2018-12-18[ssr] extended intro patterns: + > [^] /ltac:Enrico Tassi
2018-12-18Merge PR #9222: Fix classification of Set Default Proof Mode.Enrico Tassi
2018-12-18Merge PR #9160: Avoid user-given names in automatic introduction of bindersPierre-Marie Pédrot
2018-12-17Merge PR #8856: [gitlab] Test Ocaml trunk.Gaëtan Gilbert
2018-12-17Restrict body universes in delayed mode.Gaëtan Gilbert
2018-12-17Stop printing Monomorphic/Polymorphic in Print.Gaëtan Gilbert
2018-12-17Fix classification of Set Default Proof Mode.Gaëtan Gilbert
2018-12-17Merge PR #9206: [stm] join the tip of the document even when fixing a proof (...Emilio Jesus Gallego Arias
2018-12-15Avoid explicit names in binders for automatic introsJasper Hugunin
2018-12-14[dune] [gitlab] Test OCaml trunk.Emilio Jesus Gallego Arias
2018-12-13Merge PR #9193: Tests for #4509, #6202 which happen to be fixed (was a lost o...Gaëtan Gilbert
2018-12-13Merge PR #9117: Accept argument names for extra arguments with "extra scopes"Matthieu Sozeau
2018-12-13Merge PR #9032: checker: check inductive types by roundtrip through the kernel.Pierre-Marie Pédrot
2018-12-13Merge PR #9167: Fixes #9166: no deprecation warning on aliases used as patter...Pierre-Marie Pédrot
2018-12-13[test] for join when error resiliency on and async-proofs offEnrico Tassi
2018-12-13[test] for #9204Enrico Tassi
2018-12-12Accept argument names for extra arguments with "extra scopes"Maxime Dénès
2018-12-12checker: check inductive types by roundtrip through the kernel.Gaëtan Gilbert
2018-12-12Merge PR #8965: Add `String Notation` vernacular like `Numeral Notation`Hugo Herbelin
2018-12-12Fixes #9166 (no warning on pattern variables named like a deprecated alias).Hugo Herbelin
2018-12-12Merge PR #8974: Fix mod_subst wrt universe polymorphismMaxime Dénès
2018-12-11Tests for #4509, #6202 which happen to be fixed (was a lost of evars in shelf).Hugo Herbelin
2018-12-10[test-suite] Fail when the checker failsVincent Laporte
2018-12-10[test-suite] Run `coqchk` on most test casesVincent Laporte
2018-12-08Do so that an error message follows the "Error:" header on the same line.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-26 20:00:25 +0000