aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2021-02-26[coqc] Don't allow to pass more than one file to coqcEmilio Jesus Gallego Arias
This has been in the TODO queue for a long time, and indeed I have recently seen some trouble with users passing two .v files to Coq, which it isn't a) tested, b) supported. Moreover, it doesn't even work correctly in 8.13 due to some other changes in the toplevel related to auxiliary files. (*) https://stackoverflow.com/questions/66261987/compiling-multiple-coq-files-does-not-work
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]
Reviewed-by: silene Ack-by: SkySkimmer
2021-02-17Merge PR #13734: Fix #13732: Implicit Type vs universesPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-02-16[coqtop] be verbose only in interactive modeEnrico Tassi
2021-02-11Merge PR #13826: [micromega] Fixes #13794Vincent Laporte
Reviewed-by: vbgl
2021-02-10[micromega/nia] Improve sharing of proofsBESSON Frederic
Closes #13794
2021-02-04Properly handle ordering of -w and -native-compilerGaëtan Gilbert
Warnings are handled as injection commands, interleaved with options and requires. Native compiler impacts require, so we must convert "yes" to "no" before handling injections. As such the semantic handling of the native command line argument must be separated from the emission of the warning message, which this PR implements. Fix #13819 In principle the other 2 cwarning in coqargs (deprecated spropcumul and inputstate) should be moved to injections too, but since they're deprecated I can't be bothered.
2021-02-03Fix #13739 - disable some warnings when calling Function.Pierre Courtieu
Also added a generic way of temporarily disabling a warning. Also added try_finalize un lib/utils.ml.
2021-01-28Merge PR #13763: Remove the SearchHead command (deprecated in 8.12)coqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2021-01-26[vernac] Check that no proofs do remain open at section/module closing timeEmilio Jesus Gallego Arias
Fixes #13755 .
2021-01-25Remove the SearchHead commandJim Fehrle
2021-01-25Merge PR #13779: Properly implement local references in Summary.coqbot-app[bot]
Reviewed-by: gares
2021-01-25add testEnrico Tassi
2021-01-24Merge PR #13762: Remove double induction tacticPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2021-01-20Remove double induction tacticJim Fehrle
2021-01-20Merge PR #13744: Make sure "Print Module" write a dot at the end of ↵coqbot-app[bot]
inductive definitions. Reviewed-by: SkySkimmer
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-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
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-11Fix #13732: Implicit Type vs universesGaëtan Gilbert
This returns to the previous behaviour of Implicit Type forgetting universes. `Implicit Type T : Type@{u}.` may be confusing as it is equivalent to `: Type`, but until we have a better idea of what to do with anonymous types I see no other solution, especially in the short term to fix the bug.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-19 01:24:45 +0000