aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2019-12-11Merge PR #11271: Fixing #9893. "Specialize with" would not support hyps type ↵Pierre-Marie Pédrot
containing letins. Reviewed-by: ppedrot
2019-12-10Merge PR #10202: Slightly more robust manual implicit argumentsEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-12-10Fixing #9893 (Letins not supported in the specialized hypothesis).Pierre Courtieu
2019-12-05Merge PR #11241: Unfortunate Coq 8.10 bug with "cofix with" tactic syntaxEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-12-05Unfortunate bug with "cofix with": case of a CProdN over no bindings.Hugo Herbelin
Failing on CProdN([],...) was maybe a bit too radical.
2019-12-04Manual implicit arguments: more robustness tests.Hugo Herbelin
- Warn in some places where {x:T} is not assumed to occur (e.g. in argument of an application, or of a match). - Warn when an implicit argument occurs several times with the same name. - Accept local anonymous {_:T} with explicitation possible using name `arg_k`. We obtain this by using a flag (impl_binder_index) which tells if we are in a position where implicit arguments matter and, if yes, the index of the next binder.
2019-12-03Printing: Interleaving search for notations and removal of coercions.Hugo Herbelin
We renounce to the ad hoc rule preferring a notation w/o delimiter for a term with coercions stripped over a notation for the fully-applied terms with coercions not removed. Instead, we interleave removal of coercions and search for notations: we prefer a notation for the fully applied term, and, if not, try to remove one coercion, and try again a notation for the remaining term, and if not, try to remove the next coercion, etc. Note: the flatten_application could be removed if prim_token were able to apply on a prefix of an application node.
2019-12-03Merge PR #11113: Remove deprecated compat modifier of Notation / Infix commands.Emilio Jesus Gallego Arias
Reviewed-by: JasonGross Reviewed-by: ejgallego Reviewed-by: maximedenes
2019-12-03Merge PR #11162: [CS] support #[local] attributeMaxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-12-02Merge PR #11198: Display more information when complexity tests failHugo Herbelin
Reviewed-by: gares Reviewed-by: herbelin
2019-12-02Remove deprecated compat modifier of Notation / Infix commands.Théo Zimmermann
And simplify a lot the compatibility infrastructure following this. Update dev/tools/update-compat.py Remove much complexity. Co-authored-by: Jason Gross <jgross@mit.edu>
2019-12-02[CS] support #[local] attributeEnrico Tassi
2019-12-02Merge PR #10575: Clean up deprecationsThéo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: silene
2019-12-01Merge PR #11185: Remove deprecated Typeclasses Axioms Are Instances.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: cpitclaudel
2019-11-30Actually deprecate the `cutrewrite` tacticMaxime Dénès
The manual was already saying that it was deprecated, but no warning was emitted. Fixes #10572
2019-11-29Merge PR #11076: Remove all remaining calls to “omega” from the standard ↵Emilio Jesus Gallego Arias
library Reviewed-by: ejgallego
2019-11-29Remove deprecated Typeclasses Axioms Are Instances.Théo Zimmermann
2019-11-28Relax the pattern complexity testJason Gross
c.f. discussion at https://github.com/coq/coq/pull/11177#issuecomment-559139477
2019-11-27Display more information when complexity tests failJason Gross
In particular, display how long they took in bogomips-adjusted centiseconds.
2019-11-27[release] Update files for 8.12 release per release process.Emilio Jesus Gallego Arias
2019-11-27Merge PR #11128: Fix #11039: proof of False with template poly and nonlinear ↵Pierre-Marie Pédrot
universes Reviewed-by: Zimmi48 Reviewed-by: mattam82 Reviewed-by: ppedrot
2019-11-26Merge PR #11177: Add a complexity test for `pattern`Hugo Herbelin
Reviewed-by: herbelin
2019-11-26Update test-suite/complexity/pattern.vJason Gross
Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com>
2019-11-26Merge PR #11090: Printing of coercions to which a notation is associated: a ↵Emilio Jesus Gallego Arias
refined version of #8890 which prevents #11033. Ack-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares
2019-11-26Merge PR #11166: Add test for #11161Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-11-26Fix #11039: proof of False with template poly and nonlinear universesGaëtan Gilbert
Using the parameter universes in the constructor causes implicit equality constraints, so those universes may not be template polymorphic. A couple types in the stdlib were erroneously marked template, which is now detected. Removing the marking doesn't actually change behaviour though. Also fixes #10504.
2019-11-25Merge PR #11146: Combine similar arguments when printing Arguments commandHugo Herbelin
Reviewed-by: ejgallego Reviewed-by: herbelin
2019-11-25Test-suite: avoid using “omega”Vincent Laporte
2019-11-25Add a complexity test for `pattern`Jason Gross
This is to hopefully prevent regressions on https://github.com/coq/coq/issues/11150 and https://github.com/coq/coq/issues/6502.
2019-11-22Add test for #11161Gaëtan Gilbert
This is better than expecting other tests to fail if we mess up again.
2019-11-21A refined version of #8890 which prevents #11033.Hugo Herbelin
We restrict #8890 so that it looks for a notation only for the fully applied coercion.
2019-11-21Merge PR #11132: Fixing bugs in the computation of implicit arguments for ↵Emilio Jesus Gallego Arias
`Fixpoint` with a let binder Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-11-21Merge PR #11075: load .vo when .vos is missing + misc vos changesEmilio Jesus Gallego Arias
Reviewed-by: gares Reviewed-by: silene
2019-11-20Combine similar arguments when printing Arguments commandGaëtan Gilbert
"similar" means sharing a scope or implicit status.
2019-11-20From CoqIDE or -vos or -vok compilation, load .vo when .vos is missing ↵charguer
(fixing bug #11057). With this new behavior, it is not needed to .vos files in user contribs. Also, this commit adds a feature: upon creation of a .vo file, an empty .vok file is touched.
2019-11-19Fixing bugs in the computation of implicit arguments for fix with a let binder.Hugo Herbelin
2019-11-13Return of Refine Instance as an attribute.Gaëtan Gilbert
We can now do `#[refine] Instance : Bla := bli.` to enter proof mode with `bli` as a starting refinement. If `bli` is enough to define the instance we still enter proof mode, keeping things nicely predictable for the stm.
2019-11-13Merge PR #11094: Miscellaneous micro-improvements of the syntax of recordsPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-11-12Merge PR #11045: Forbid Include inside sectionsPierre-Marie Pédrot
Ack-by: Blaisorblade Reviewed-by: gares Reviewed-by: ppedrot
2019-11-11Run update-compat script with --release option.Théo Zimmermann
This should ideally have been done before the 8.11 branching.
2019-11-11Merge PR #11052: Fix #11048: uncaught destKO in inductive typePierre-Marie Pédrot
Reviewed-by: ppedrot
2019-11-11Miscellaneous improvements of the syntax of records.Hugo Herbelin
- only one space instead of two when printing "{| |}" - removing a redundant clause in the grammar of record_patterns
2019-11-10Merge PR #10980: Fix #10903: type-in-type allows fixpoints on sprop inductivesPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-11-08Merge PR #11014: Fix #8459: anomaly not enough abstractions in fix bodyPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-11-07Merge PR #11049: Prevent redefinition of Ltac2 types and constructors inside ↵Pierre-Marie Pédrot
a module Reviewed-by: ppedrot
2019-11-06Swap parsing precedence of `::` and `,` ; Fix #10116Kenji Maillard
2019-11-05Fixing test-suiteKenji Maillard
2019-11-05Fix #11048: uncaught destKO in inductive typeGaëtan Gilbert
Reduction.whd_all does not commute with to_constr.
2019-11-05Forbid Include inside sectionsGaëtan Gilbert
This probably does not work well in general, and specifically avoids an anomaly fixing https://github.com/coq/coq/issues/10060
2019-11-04Prevent double definition of Ltac2 constructors inside a module; Fix #11046Kenji Maillard
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-26 01:40:51 +0000