aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2021-03-31Merge PR #14035: Fix printing of ssr do intros and seq tacticscoqbot-app[bot]
2021-03-31Fix printing of ssr do intros and seq tacticsLasse Blaauwbroek
2021-03-30Properly expand projection parameters in Btermdn.Pierre-Marie Pédrot
2021-03-30Merge PR #14012: Fix Ltac2 `Array.init` exponential overheadPierre-Marie Pédrot
2021-03-26Add non-performance-based testJason Gross
2021-03-26Be more thorough when testing PArray.set.Guillaume Melquiond
2021-03-26Fix Ltac2 `Array.init` exponential overheadJason Gross
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-17 19:52:37 +0000