aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2021-02-26[coqc] Don't allow to pass more than one file to coqcEmilio Jesus Gallego Arias
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
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-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
2021-01-09Merge PR #13299: Remember universe instances of constants in notationscoqbot-app[bot]
2021-01-07Merge PR #13696: Deprecate "at ... with ..." in change tactic (use "with ... ...Pierre-Marie Pédrot
2021-01-07Merge PR #13715: [micromega] Add missing support for `implb`Vincent Laporte
2021-01-06[micromega] Add missing support for `implb`BESSON Frederic
2021-01-04Remember universe instances of constants in notationsJasper Hugunin
2021-01-04Temporarily deactivating printing check for cases.Pierre-Marie Pédrot
2021-01-04EConstr iterators respect the binding structure of cases.Pierre-Marie Pédrot
2021-01-02Deprecate "at ... with ..." in change tacticJim Fehrle
2020-12-31Adding a test for conversion involving let-bindings in inductive parameters.Pierre-Marie Pédrot
2020-12-31Add a test for a complex conversion involving pattern-matching with let-bindi...Pierre-Marie Pédrot
2020-12-28Fix broken HTML rendering of inference rules (fix #12783).Guillaume Melquiond
2020-12-17Add a test for change over case nodes.Pierre-Marie Pédrot
2020-12-16Merge PR #13568: Fix #13566: Add checks for invalid occurrences in several ta...Pierre-Marie Pédrot
2020-12-14Add checks for invalid occurrences in setoid rewrite.Hugo Herbelin
2020-12-14Merge PR #13523: [envars] honor file "coq_environment.txt"Pierre-Marie Pédrot
2020-12-13Removing flag "Bracketing Last Introduction Pattern".Hugo Herbelin
2020-12-11Merge PR #13519: Better primitive type support in custom string and numeral n...coqbot-app[bot]
2020-12-09Constrintern: Code factorization in interning of record fields.Hugo Herbelin
2020-12-09Fixing support for argument scopes and let-ins while interning cases patterns.Hugo Herbelin
2020-12-08Merge PR #13597: Congruence: don't replace error messages by "congruence failed"coqbot-app[bot]
2020-12-08Congruence: don't replace error messages by "congruence failed"Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:00:21 +0000