aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2020-11-03Merge PR #13256: Remove test-suite/bugs/opened/bug_3395.v: not a bugcoqbot-app[bot]
Reviewed-by: herbelin
2020-11-03Merge PR #13092: Fixing #13078: stack overflow and anomalies with binding ↵coqbot-app[bot]
notations in patterns Reviewed-by: ejgallego Ack-by: ppedrot Ack-by: LasseBlaauwbroek
2020-11-03Fix test-suite in async mode.Théo Zimmermann
(By closing unfinished proofs.)
2020-11-02Nicer spacing when printing array literalsGaëtan Gilbert
From [|x; y; z | def : ty |] to [| x; y; z | def : ty |]
2020-11-02Fix printing for empty primitive arraysGaëtan Gilbert
Fix #13178
2020-11-02Merge PR #13183: attribute #[using] for Definition and Fixpointcoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: herbelin Ack-by: Zimmi48
2020-11-02Merge PR #13274: Fix two bugs in conversion of primitive valuescoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-02Merge PR #13247: Fixes #13241: nested Ltac functions wrongly reporting error ↵Pierre-Marie Pédrot
on the inner calls Reviewed-by: ppedrot
2020-11-02[stm] support #[using] attributeEnrico Tassi
2020-11-02attribute #[using] for Definition and FixpointEnrico Tassi
2020-10-31Closes #13278: take into account elimination constraints in small inversion.Hugo Herbelin
Ideally, if equations t <= ?x were preserving subtyping that could be simpler. Currently we need however to put a rigid universe as constraint on the return predicate so that one branch does not force the return sort to be lower by unification than what another branch would have needed.
2020-10-31Fine-tuning the sort of the predicate obtained by small inversion.Hugo Herbelin
If the result is in SProp, Prop or (impredicative) Set, we preserve this information since the elimination sort might be restricted by the sort of the destructed type. If the result is in Type, we use a fresh sort upper bound so that we are sure not having residual algebraic universes which would raise problems in a type constraint (e.g. in define_evar_as_product). This fixes the part of #13278 posted on discourse.
2020-10-30Renaming Numeral.v into Number.vPierre Roux
2020-10-29Fixing interpretation of rewrite_strat argument in Ltac.Hugo Herbelin
Ltac variables were not yet supported.
2020-10-29Use same code for "Print Ltac foo" and "Print foo" when "foo" is an Ltac.Hugo Herbelin
Adopting the same format means printing "Ltac foo := ..." and not the fully qualified name of foo.
2020-10-28Fixes #13241 (nested Ltac functions were wrongly reporting error on the ↵Hugo Herbelin
inner calls). This continues #12223, #12773, #12992, #12774, #12999.
2020-10-27Merge PR #13238: Fix some tactic print bugscoqbot-app[bot]
Reviewed-by: gares Reviewed-by: herbelin Ack-by: ppedrot
2020-10-27Rename operconstr -> termJim Fehrle
2020-10-26Merge PR #12768: Granting wish #12762: warning on duplicated catch-all ↵coqbot-app[bot]
pattern-matching clause with unused named variable Reviewed-by: jfehrle Reviewed-by: vbgl Ack-by: gares
2020-10-26Adding a test for the second bug.Pierre-Marie Pédrot
2020-10-22Remove test-suite/bugs/opened/bug_3395.v: not a bugGaëtan Gilbert
2020-10-22Fix printing of wit_constr and some ssr problems with printing empty listsLasse Blaauwbroek
2020-10-22Merge PR #13130: setoid_rewrite: record generated name when rewriting under ↵Pierre-Marie Pédrot
lambda Reviewed-by: ppedrot
2020-10-21Merge PR #13118: [type classes] Simplify cl_contextPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-21Merge PR #13201: Report a useful error for dependent destructionPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-21Merge PR #12955: Reroot primitive arrays on accesscoqbot-app[bot]
Reviewed-by: maximedenes
2020-10-20[zify] Add support for Int63.intFrédéric Besson
Update doc/sphinx/addendum/micromega.rst Co-authored-by: Jason Gross <jasongross9@gmail.com> Update theories/micromega/ZifyInt63.v Co-authored-by: Jason Gross <jasongross9@gmail.com>
2020-10-19Merge PR #13166: Fixes #13165: implicit arguments in defined fields of ↵coqbot-app[bot]
record types not taken into account Reviewed-by: SkySkimmer
2020-10-19Merge PR #13207: Use list notation in examples referenced by "nsatz" ↵coqbot-app[bot]
documentation Reviewed-by: Zimmi48
2020-10-19Addressing parsing part #13078.Hugo Herbelin
We don't give sense to pattern/binders in leftmost position.
2020-10-19Fixing printing part of #13078 (anomaly with binding notations in patterns).Hugo Herbelin
We prevent notations involving binders (i.e. names or patterns) to be used for printing in "match" patterns. The computation is done in "has_no_binders_type", controlling uninterpretation.
2020-10-19Merge PR #13192: Fix algebraic on the right when using bidi hintscoqbot-app[bot]
Reviewed-by: gares
2020-10-16Use list notation in nsatz examples referenced in the docJim Fehrle
2020-10-16Fixes/enhancements with local definitions in records.Hugo Herbelin
Fixes implicit arguments from the body of a defined field not taken into account. Get (a bit) more information for detection of SProp relevance in implicitly-typed defined field. (It should be done at the very end of the inference phase, though, because some evars may not yet be instantiated.)
2020-10-15Merge PR #12925: [declare] Fix types of mutual lemmas when using Admitted.coqbot-app[bot]
Reviewed-by: herbelin Ack-by: SkySkimmer
2020-10-15Report a useful error for dependent destructionTej Chajed
Similar to `dependent induction`, report an error message for `dependent destruction` saying that importing `Coq.Program.Equality` is required, rather than failing at parsing time. This is a small extension of #605 to cover dependent destruction as well. Here I also put in some tests.
2020-10-15Merge PR #13181: Guard unify_leq_delay calls in TypingPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-15Merge PR #13140: Documenting Set Printing Goal Names + a small goal display fixcoqbot-app[bot]
Reviewed-by: ejgallego Reviewed-by: Zimmi48
2020-10-15Merge PR #13144: Closes #13142: more standardized pretty-printing of Coq recordscoqbot-app[bot]
Reviewed-by: ejgallego Ack-by: SkySkimmer
2020-10-15[declare] Fix types of mutual lemmas when using Admitted.Emilio Jesus Gallego Arias
We fix a clear coding mistake in 79bcf1c0a22e736c4e2cae3460c35b3d9fca9aa0 that forgot to update the type of the parameter entry when saving mutual definitions without a body. We follow the solution suggested by Hugo Herbelin and drop the type used in `start_proof`. Note the duplication here indeed. Fixes #12895 Co-authored-by: Hugo Herbelin <Hugo.Herbelin@inria.fr>
2020-10-14Fix algebraic on the right when using bidi hintsGaëtan Gilbert
Fix #12970 We can't recover the expected type of the post bidi argument by retyping because the hole may be filled by something in which case retyping can produce algebraic universes.
2020-10-14Fix anomaly when importing a functorGaëtan Gilbert
Fix #13162
2020-10-13Merge PR #13172: Fix #13169: vm_compute has existential crisis.coqbot-app[bot]
Reviewed-by: silene
2020-10-12Merge PR #12874: Add a "Show Proof Diffs" message to the XML protocolcoqbot-app[bot]
Reviewed-by: herbelin Ack-by: gares Ack-by: ejgallego
2020-10-12Check types when converting irrelevant terms in old unificationGaëtan Gilbert
Fixes probably many strange issues such as the example in #13171
2020-10-12Guard unify_leq_delay calls in TypingGaëtan Gilbert
Fix #13171
2020-10-12Merge PR #12449: Minimize Prop <= i to i := Setcoqbot-app[bot]
Reviewed-by: mattam82 Ack-by: Janno Ack-by: gares
2020-10-11Fix #13169: vm_compute has existential crisis.Pierre-Marie Pédrot
We simply use evars instance in the right order while reading back VM values.
2020-10-10New spacing/formatting in Locate Notation, Print Scopes, Print Visibility.Hugo Herbelin
2020-10-10Notations: reworking the treatment of only-parsing and only-printing notations.Hugo Herbelin
The (old) original model for notations was to associated both a parsing and a printing rule to a notation. Progressively, it become more and more common to have only parsing notations or even multiple expressions printed with the same notation. The new model is to attach to a given scope, string and entry at most one either only-parsing or mixed-parsing-printing rules + an arbitrarily many unrelated only-printing rules. Additionally, we anticipate the ability to selectively activate/deactivate each of those. This allows to fix in particular #9682 but also to have more-to-the-point warnings in case a notation overrides or partially overrides another one. Rules for importing are not changed (see forthcoming #12984 though). We also improve the output of "Print Scopes" so that it adds when a notation is only-parsing, only-printing, or deactivated, or a combination of those. Fixes #4738 Fixes #9682 Fixes part 2 of #12908 Fixes #13112
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-14 12:43:51 +0000