aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2021-03-26Never store persistent arrays as VM structured values.Pierre-Marie Pédrot
2021-03-25Merge PR #14004: Fix the redeclaration check for Ltac2 entry points.coqbot-app[bot]
2021-03-25Merge PR #13909: Minimize the set of multiple inheritance (coercion) paths to...coqbot-app[bot]
2021-03-25Merge PR #13852: [vernac] Improve alpha-renaming in record projection typescoqbot-app[bot]
2021-03-25Fix the redeclaration check for Ltac2 entry points.Pierre-Marie Pédrot
2021-03-24Merge PR #13968: implement is_const, is_var, ... etc and has_evar for Ltac2Pierre-Marie Pédrot
2021-03-23Merge PR #13774: Allow to register deprecation status in Ltac2 term and notat...Michael Soegtrop
2021-03-23Merge PR #13914: Allow the presence of type casts for return values in Ltac2.Michael Soegtrop
2021-03-22Merge PR #13961: Implement ! goal selector for Ltac2.coqbot-app[bot]
2021-03-19implement is_const, is_var, ... etc and has_evar for Ltac2Samuel Gruetter
2021-03-19Merge PR #13924: Fix kernel incorrectly assuming the "using" hyps are transit...Pierre-Marie Pédrot
2021-03-18Implement ! goal selector for Ltac2.Pierre-Marie Pédrot
2021-03-16Slightly richer API allowing to shift the inductive in a block.Pierre-Marie Pédrot
2021-03-16Add tests for the new Ltac2 Ind API.Pierre-Marie Pédrot
2021-03-13Minimize the set of multiple inheritance paths to check for conversionKazuhiko Sakaguchi
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 22:47:29 +0000