aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Expand)Author
2021-04-23Merge PR #13965: [abbreviation] user syntax to set interp scope of argumentPierre-Marie Pédrot
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-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-16Merge PR #13939: Allow scope delimiters in Ltac2 open_constr:(...) quotation.coqbot-app[bot]
2021-04-07[abbreviation] allow the user to set arguments scopeEnrico Tassi
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-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-26Fix Ltac2 `Array.init` exponential overheadJason Gross
2021-03-26Never store persistent arrays as VM structured values.Pierre-Marie Pédrot
2021-03-25Fix the redeclaration check for Ltac2 entry points.Pierre-Marie Pédrot
2021-03-22Merge PR #13961: Implement ! goal selector for Ltac2.coqbot-app[bot]
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-13Allow scope delimiters in Ltac2 open_constr:(...) quotation.Pierre-Marie Pédrot
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-06Merge PR #13586: Support nested timeoutsPierre-Marie Pédrot
2021-03-04Properly support nested timeoutsLasse Blaauwbroek
2021-03-04Fix #12011 ssreflect "rewrite in" with setoidsGaëtan Gilbert
2021-02-26[coqc] Don't allow to pass more than one file to coqcEmilio Jesus Gallego Arias
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-17Merge PR #13734: Fix #13732: Implicit Type vs universesPierre-Marie Pédrot
2021-01-26[vernac] Check that no proofs do remain open at section/module closing timeEmilio Jesus Gallego Arias
2021-01-18Fixes #13413: freshness issue with "%" introduction pattern.Hugo Herbelin
2021-01-11Fix #13732: Implicit Type vs universesGaëtan Gilbert
2021-01-09Merge PR #13299: Remember universe instances of constants in notationscoqbot-app[bot]
2021-01-04Remember universe instances of constants in notationsJasper Hugunin
2021-01-04EConstr iterators respect the binding structure of cases.Pierre-Marie Pédrot
2020-12-13Removing flag "Bracketing Last Introduction Pattern".Hugo Herbelin
2020-11-30Merge PR #13501: [kernel] Fix #13495: incompleteness in cases typing for cumu...coqbot-app[bot]
2020-11-28Merge PR #13502: A small fix for freshness in the `change` tacticcoqbot-app[bot]
2020-11-27[kernel] Fix #13495: incompleteness in cases typing for cumulative inductive ...Matthieu Sozeau
2020-11-27A small fix for freshness in the `change` tacticJasper Hugunin
2020-11-27Merge PR #13468: Fixes #13456: regression in tactic exists which started to c...Pierre-Marie Pédrot
2020-11-26Fixes #13456: regression where tactic exists started to check evars increment...Hugo Herbelin
2020-11-25Add tests for #13303Gaëtan Gilbert
2020-11-24Merge PR #13455: Fix comparison of extracted array literalscoqbot-app[bot]
2020-11-24Merge PR #13444: Fixes another instance of bug #7967 and #8076: restriction o...coqbot-app[bot]
2020-11-23Fix comparison of extracted array literalsGaëtan Gilbert
2020-11-22Adapting standard library, doc and test suite to ident->name renaming.Hugo Herbelin
2020-11-22Fixes another instance of bug #7967: restriction of universes in "Context".Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:36:37 +0000