aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2021-04-21Merge PR #14094: Properly pass the Ltac2 notation level to the gramlib API.coqbot-app[bot]
2021-04-20Merge PR #14131: Check for existence before using `Global.lookup_constant` in...Pierre-Marie Pédrot
2021-04-20Merge PR #14089: unify for Ltac2Pierre-Marie Pédrot
2021-04-19Merge PR #14108: [zify] bugfixVincent Laporte
2021-04-19Check for existence before using `Global.lookup_constant` instead of catching...Lasse Blaauwbroek
2021-04-17Properly pass the Ltac2 notation level to the gramlib API.Pierre-Marie Pédrot
2021-04-16[zify] bugfixFrederic Besson
2021-04-16Merge PR #13939: Allow scope delimiters in Ltac2 open_constr:(...) quotation.coqbot-app[bot]
2021-04-14Merge PR #14050: Remove remote counter systemcoqbot-app[bot]
2021-04-14Add test for -schedule-vio-checkingGaëtan Gilbert
2021-04-14Remove remote counter systemGaëtan Gilbert
2021-04-14Put async worker id in universe namesGaëtan Gilbert
2021-04-12[zify] More aggressive application of saturation rulesBESSON Frederic
2021-04-12Merge PR #14061: [zify] better error reportingVincent Laporte
2021-04-12[zify] better error reportingBESSON Frederic
2021-04-08remove `with hintdb` variant of Ltac2 `unify`, becauseSamuel Gruetter
2021-04-07unify for Ltac2Samuel Gruetter
2021-04-06Merge PR #13741: Remove omega tactic (deprecated in 8.12)coqbot-app[bot]
2021-04-04More extraction tests for inductive types with let-ins.Hugo Herbelin
2021-04-04Fixing #13581: missing support for let-ins in arity of inductive types.Hugo Herbelin
2021-04-02Remove the omega tactic and related optionsJim Fehrle
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-13Allow scope delimiters in Ltac2 open_constr:(...) quotation.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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:52:48 +0000