aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2021-01-20Remove double induction tacticJim Fehrle
2021-01-19Merge PR #13699: Fix #13579 (hnf on primitives raises an anomaly)Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2021-01-19Merge PR #13512: Fixes #13413: freshness failure in apply-in introduction ↵Pierre-Marie Pédrot
pattern Reviewed-by: ppedrot
2021-01-19Merge PR #13725: Support locality attributes for Hint Rewrite (including export)Pierre-Marie Pédrot
Ack-by: Zimmi48 Ack-by: gares Reviewed-by: ppedrot
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
We build earlier the final expected name at the end of a sequence of "%" introduction patterns.
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
We deprecate unspecified locality as was done for Hint. Close #13724
2021-01-18Fix #13579 (hnf on primitives raises an anomaly)Pierre Roux
Also works for simpl.
2021-01-13Avoid using "subgoals" in the UI, it means the same as "goals"Jim Fehrle
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
The arity of a destructuring let in a pattern is allowed to be shorter than the case term node it actually matches. This is an unexpected side-effect of the legacy expanded representation of cases that happens to be relied upon in the wild, as evidenced by the CI failures from #13723.
2021-01-09Merge PR #13299: Remember universe instances of constants in notationscoqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: herbelin
2021-01-07Merge PR #13696: Deprecate "at ... with ..." in change tactic (use "with ... ↵Pierre-Marie Pédrot
at ..." instead) Ack-by: Zimmi48 Reviewed-by: ppedrot
2021-01-07Merge PR #13715: [micromega] Add missing support for `implb`Vincent Laporte
Reviewed-by: vbgl
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
Destruct has changed semantics, but I'd like to see how CI fares so far.
2021-01-04EConstr iterators respect the binding structure of cases.Pierre-Marie Pédrot
Fixes #3166.
2021-01-02Deprecate "at ... with ..." in change tacticJim Fehrle
(use "with ... at ..." instead)
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 ↵Pierre-Marie Pédrot
let-bindings.
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
This is extracted from #13563.
2020-12-16Merge PR #13568: Fix #13566: Add checks for invalid occurrences in several ↵Pierre-Marie Pédrot
tactics. Reviewed-by: ppedrot
2020-12-14Add checks for invalid occurrences in setoid rewrite.Hugo Herbelin
We additionally check that occurrence 0 is invalid in simpl at, unfold at, etc.
2020-12-14Merge PR #13523: [envars] honor file "coq_environment.txt"Pierre-Marie Pédrot
Reviewed-by: MSoegtropIMC Reviewed-by: Zimmi48 Ack-by: ejgallego Ack-by: herbelin Ack-by: ppedrot
2020-12-13Removing flag "Bracketing Last Introduction Pattern".Hugo Herbelin
2020-12-11Merge PR #13519: Better primitive type support in custom string and numeral ↵coqbot-app[bot]
notations. Reviewed-by: jfehrle Reviewed-by: proux01 Ack-by: Zimmi48 Ack-by: SkySkimmer
2020-12-09Constrintern: Code factorization in interning of record fields.Hugo Herbelin
Also includes some fine-tuning of error messages.
2020-12-09Fixing support for argument scopes and let-ins while interning cases patterns.Hugo Herbelin
We also simplify the whole process of interpretation of cases pattern on the way.
2020-12-08Merge PR #13597: Congruence: don't replace error messages by "congruence failed"coqbot-app[bot]
Reviewed-by: ejgallego Ack-by: PierreCorbineau
2020-12-08Congruence: don't replace error messages by "congruence failed"Gaëtan Gilbert
Fix #13595
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]
Reviewed-by: Zimmi48 Ack-by: jfehrle
2020-12-06Fix spelling in warning entrySimon Friis Vindum
2020-12-04Merge PR #13552: Delay inventing names for monomorphic universesPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-12-04Merge PR #13442: Add an abstraction function in the LtacX FFI.coqbot-app[bot]
Reviewed-by: kyoDralliam
2020-12-04Delay inventing names for monomorphic universesGaëtan Gilbert
This avoids doing it repeatedly for nothing in intern/extern.
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
On windows we provide a way to set environment variables local to a coq installation by providing a file named "coq_environment.txt" containing KEY="value" pairs. No space between KEY and = is allowed, values are in quotes according to OCaml's escaping conventions. The file is line-directed, illformed lines are skipped.
2020-12-04Better primitive type support in custom string and numeral notations.Fabian Kunze
- float and array values are now supported for printing and parsing in custom notations (and in notations defined using the ocaml API) - the three constants bound to the primitive float, int and array type are now allowed anywhere inside a term to print, to handle them similar to `real` type constructors - Grants #13484: String notations for primitive arrays - Fixes #13517: String notation printing fails with primitive integers inside lists
2020-12-02Merge PR #13275: Put all Int63 primitives in a separate fileVincent Laporte
Ack-by: SkySkimmer Ack-by: ppedrot Reviewed-by: vbgl
2020-12-02Put all Int63 primitives in a separate filePierre Roux
Following a request from Pierre-Marie Pédrot in #13258
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 ↵coqbot-app[bot]
cumulative inductive types Reviewed-by: SkySkimmer
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]
Reviewed-by: herbelin
2020-11-27Merge PR #12586: [declare] Allow custom typing flags when declaring constants.coqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: gares Reviewed-by: herbelin Ack-by: jfehrle
2020-11-27[kernel] Fix #13495: incompleteness in cases typing for cumulative inductive ↵Matthieu Sozeau
types
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-07 23:50:12 +0000