aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
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
2020-12-08Add a test for cbv over inductive types which feature let-bindings.Pierre-Marie Pédrot
2020-12-07Merge PR #13556: Fix spelling in warning entrycoqbot-app[bot]
2020-12-06Fix spelling in warning entrySimon Friis Vindum
2020-12-04Merge PR #13552: Delay inventing names for monomorphic universesPierre-Marie Pédrot
2020-12-04Merge PR #13442: Add an abstraction function in the LtacX FFI.coqbot-app[bot]
2020-12-04Delay inventing names for monomorphic universesGaëtan Gilbert
2020-12-04[dune] [test-suite] pass BIN= as the regular makefile doesEnrico Tassi
2020-12-04[test-suite] improve ocaml_pwdEnrico Tassi
2020-12-04[win] [envars] honor file "coq_environment.txt"Enrico Tassi
2020-12-04Better primitive type support in custom string and numeral notations.Fabian Kunze
2020-12-02Merge PR #13275: Put all Int63 primitives in a separate fileVincent Laporte
2020-12-02Put all Int63 primitives in a separate filePierre Roux
2020-11-30Add test for this new function.Pierre-Marie Pédrot
2020-11-30Merge PR #13501: [kernel] Fix #13495: incompleteness in cases typing for cumu...coqbot-app[bot]
2020-11-29Fixing printing of apply in (continuation of #12246).Hugo Herbelin
2020-11-28Merge PR #13502: A small fix for freshness in the `change` tacticcoqbot-app[bot]
2020-11-27Merge PR #12586: [declare] Allow custom typing flags when declaring constants.coqbot-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 #13473: Testing {in _, _} and {pred _} from ssrboolcoqbot-app[bot]
2020-11-27Merge PR #13468: Fixes #13456: regression in tactic exists which started to c...Pierre-Marie Pédrot
2020-11-27Merge PR #13457: [RM] Update magicno & compatcoqbot-app[bot]
2020-11-26[attributes] [typing] Rename `typing` to `bypass_check`Emilio Jesus Gallego Arias
2020-11-26[attributes] [doc] Documentation review by Théo.Emilio Jesus Gallego Arias
2020-11-26[proofs] Support per-definition typing-flags in interactive proofs.Emilio Jesus Gallego Arias
2020-11-26[vernac] Allow to control typing flags with attributes.Emilio Jesus Gallego Arias
2020-11-26Fixes #13456: regression where tactic exists started to check evars increment...Hugo Herbelin
2020-11-26Merge PR #13415: Separate interning and pretyping of universescoqbot-app[bot]
2020-11-26Merge PR #13379: Add a new evar source to refer to evars which are types of e...coqbot-app[bot]
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:10:12 +0000