aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2021-03-12Algorithmically faster algorithm for term replacing.Pierre-Marie Pédrot
2021-03-11Merge PR #13854: Normalize evars during bytecode compilation.coqbot-app[bot]
2021-03-10Fix kernel incorrectly assuming the "using" hyps are transitively closedGaëtan Gilbert
2021-03-10Merge PR #13840: [notation] option to fine tune printing of literalscoqbot-app[bot]
2021-03-10Adding output tests.Pierre-Marie Pédrot
2021-03-10Adding a parsing test.Pierre-Marie Pédrot
2021-03-09Replace cl_index with cl_typ in coercionops.mlKazuhiko Sakaguchi
2021-03-06[vernac] Improve alpha-renaming in record projection typesLi-yao Xia
2021-03-06Merge PR #13586: Support nested timeoutsPierre-Marie Pédrot
2021-03-06Merge PR #13882: Fix #12011 ssreflect "rewrite in" with setoidsPierre-Marie Pédrot
2021-03-06Merge PR #13236: Add a type of format strings to Ltac2.Michael Soegtrop
2021-03-04Properly support nested timeoutsLasse Blaauwbroek
2021-03-04[test-suite] test for primitive tokens in patternsEnrico Tassi
2021-03-04[notation] option to fine tune printing of literalsEnrico Tassi
2021-03-04Fix #12011 ssreflect "rewrite in" with setoidsGaëtan Gilbert
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
2021-02-27Merge PR #13876: [coqc] Don't allow to pass more than one file to coqccoqbot-app[bot]
2021-02-26[coqc] Don't allow to pass more than one file to coqcEmilio Jesus Gallego Arias
2021-02-26Signed primitive integersAna
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
2021-02-24Use Reductionops.clos_whd_flags in vm_compute and native_compute.Guillaume Melquiond
2021-02-23Normalize evars during bytecode compilation (fix #13841).Guillaume Melquiond
2021-02-19Merge PR #13865: [coqtop] be verbose only in interactive modecoqbot-app[bot]
2021-02-17Merge PR #13734: Fix #13732: Implicit Type vs universesPierre-Marie Pédrot
2021-02-16[coqtop] be verbose only in interactive modeEnrico Tassi
2021-02-11Merge PR #13826: [micromega] Fixes #13794Vincent Laporte
2021-02-10[micromega/nia] Improve sharing of proofsBESSON Frederic
2021-02-04Properly handle ordering of -w and -native-compilerGaëtan Gilbert
2021-02-03Fix #13739 - disable some warnings when calling Function.Pierre Courtieu
2021-01-28Merge PR #13763: Remove the SearchHead command (deprecated in 8.12)coqbot-app[bot]
2021-01-26[vernac] Check that no proofs do remain open at section/module closing timeEmilio Jesus Gallego Arias
2021-01-25Remove the SearchHead commandJim Fehrle
2021-01-25Merge PR #13779: Properly implement local references in Summary.coqbot-app[bot]
2021-01-25add testEnrico Tassi
2021-01-24Merge PR #13762: Remove double induction tacticPierre-Marie Pédrot
2021-01-22Add tests for the printf feature.Pierre-Marie Pédrot
2021-01-20Remove double induction tacticJim Fehrle
2021-01-20Merge PR #13744: Make sure "Print Module" write a dot at the end of inductive...coqbot-app[bot]
2021-01-19Merge PR #13699: Fix #13579 (hnf on primitives raises an anomaly)Pierre-Marie Pédrot
2021-01-19Merge PR #13512: Fixes #13413: freshness failure in apply-in introduction pat...Pierre-Marie Pédrot
2021-01-19Merge PR #13725: Support locality attributes for Hint Rewrite (including export)Pierre-Marie Pédrot
2021-01-18Preventing internal temporary names to impact the "?H"-like intro-pattern names.Hugo Herbelin
2021-01-18Fixes #13413: freshness issue with "%" introduction pattern.Hugo Herbelin
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
2021-01-18Fix #13579 (hnf on primitives raises an anomaly)Pierre Roux
2021-01-13Avoid using "subgoals" in the UI, it means the same as "goals"Jim Fehrle
2021-01-13Make sure "Print Module" write a dot at the end of inductive definitions.Guillaume Melquiond
2021-01-12Add a test for bound variables in match goal over a case involving variables.Pierre-Marie Pédrot
2021-01-11Add a test for a weird behaviour of tactic matching.Pierre-Marie Pédrot
2021-01-11Fix #13732: Implicit Type vs universesGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:01:01 +0000