aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
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
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]
Reviewed-by: gares
2020-11-27Merge PR #13468: Fixes #13456: regression in tactic exists which started to ↵Pierre-Marie Pédrot
check resolution of evars more incrementally Ack-by: SkySkimmer Reviewed-by: gares Ack-by: ppedrot
2020-11-27Merge PR #13457: [RM] Update magicno & compatcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-26[attributes] [typing] Rename `typing` to `bypass_check`Emilio Jesus Gallego Arias
As discussed in the Coq meeting.
2020-11-26[attributes] [doc] Documentation review by Théo.Emilio Jesus Gallego Arias
Co-authored-by: <Théo Zimmermann <theo.zimmermann@inria.fr>
2020-11-26[proofs] Support per-definition typing-flags in interactive proofs.Emilio Jesus Gallego Arias
Most cases should be accounted in proof code, however be wary of paths where `Global.env ()` is used.
2020-11-26[vernac] Allow to control typing flags with attributes.Emilio Jesus Gallego Arias
The syntax is the one of boolean attributes, that is to say `#[typing($flag={yes,no}]` where `$flag` is one of `guarded`, `universes`, `positive`. We had to instrument the pretyper in a few places, it is interesting that it is doing so many checks.
2020-11-26Fixes #13456: regression where tactic exists started to check evars ↵Hugo Herbelin
incrementally. The regression was due to #12365. We fix it by postponing the evars check after the calls to the underlying constructor tactic, while retaining using information from the first instantiations to resolve the latter instantiations.
2020-11-26Merge PR #13415: Separate interning and pretyping of universescoqbot-app[bot]
Reviewed-by: mattam82
2020-11-26Merge PR #13379: Add a new evar source to refer to evars which are types of ↵coqbot-app[bot]
evars Reviewed-by: SkySkimmer
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:01:39 +0000