aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
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-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-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
2020-10-10Closes #13142 (more standardized pretty-printing of records).Hugo Herbelin
2020-10-09Add an XML message for "Show Proof Diffs"Jim Fehrle
Add menu item that uses this
2020-10-09No bidirectionality when expected type for lambda is an evar.Gaëtan Gilbert
This fixes #12623 (bidirectionality breaks impredicativity).
2020-10-09Minimize Prop <= i to i := SetGaëtan Gilbert
Fix part of #8196, fix #12414 Replaces #9343
2020-10-09Merge PR #13087: Put type-in-type flag in ugraph.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-08Merge PR #12949: When a notation is only parsing, do not attach to it a ↵coqbot-app[bot]
specific format. Reviewed-by: ejgallego
2020-10-07Merge PR #13115: Derive Inversion does not allow leftover evarsPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-06Fixing redundant outputs when printing goals, especially in non-"pr_first" mode.Hugo Herbelin
Here is an example (see test output/goal_output.v for other examples): 2 subgoals, subgoal 1 (?Goal) subgoal 1 (?Goal) is: True subgoal 2 (?Goal0) is: True This is now: 2 subgoals subgoal 1 (?Goal) is: True subgoal 2 (?Goal0) is: True
2020-10-04Merge PR #13096: Drop prefixes from non-terminal names, e.g. "constr:constr" ↵coqbot-app[bot]
-> "constr" Reviewed-by: herbelin Ack-by: Zimmi48
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-10-02Merge PR #13106: Remove the forward class hint feature.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-10-01Merge PR #13114: Reimplement Admit Obligations using standard Admitted codecoqbot-app[bot]
Reviewed-by: ejgallego
2020-10-01Merge PR #13123: Fix combining uniform parameters and mutual inductives.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-09-30Fix combining uniform parameters and mutual inductives.Jasper Hugunin
2020-09-30Remove the forward class hint feature.Pierre-Marie Pédrot
It was not documented, not properly tested and thus likely buggy. Judging from the code alone I spotted already one potential bug. Further more it was prominently making use of the infamous "arbitrary term as hint" feature. Since the only user in our CI seems to be a math-classes file that introduced the feature under a claim of "cleanup", I believe we can safely remove it without anyone noticing.
2020-09-30Derive Inversion does not allow leftover evarsGaëtan Gilbert
Fix #12917
2020-09-30Reimplement Admit Obligations using standard Admitted codeGaëtan Gilbert
Fix #13109
2020-09-28Merge PR #12946: Fixes part 1 of #12908: undetected collision involving a ↵coqbot-app[bot]
lonely notation at printing time. Reviewed-by: ejgallego Ack-by: maximedenes
2020-09-28Put type-in-type flag in ugraph.Gaëtan Gilbert
Fix #13086.
2020-09-28Merge PR #13053: [lib] make canonical_path_name always absolute (fix #13031)Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-09-25Merge PR #12999: More improvements in locating tactic errorscoqbot-app[bot]
Reviewed-by: ppedrot Reviewed-by: ejgallego
2020-09-23Merge PR #13073: A temporary fix of #13018 and #12775 for branch 8.12 (bis)coqbot-app[bot]
Reviewed-by: ejgallego
2020-09-23Merge PR #13028: Fixes #9716 and #13004: don't drop the qualifier of ↵Pierre-Marie Pédrot
quotations at printing time Reviewed-by: ppedrot
2020-09-23Merge PR #12847: Tactics inversion and replace work with eq in typePierre-Marie Pédrot
Reviewed-by: ppedrot
2020-09-22Merge PR #12960: Fixes #9403 and #10803: missing flattening of nested ↵coqbot-app[bot]
applications in notations Reviewed-by: ejgallego Ack-by: maximedenes
2020-09-22Fixes #9716, #13004: don't drop the qualifier of quotations at printing time.Hugo Herbelin
2020-09-21Make print-pretty-timed robust against non-output-sync logsJason Gross
Also pass `--output-sync` on the CI, as suggested in https://github.com/coq/coq/pull/12653#issuecomment-696226093, to protect against this failure mode. Fixes #13062
2020-09-18[lib] make canonical_path_name always absolute (fix #13031)Enrico Tassi
2020-09-17Formally deprecate the double induction tactic.Pierre-Marie Pédrot
The doc states it is deprecated since 1386cd9 but this was ages before the deprecation mechanism existed.
2020-09-16Merge PR #13008: Use fresher names in eqschemesHugo Herbelin
Reviewed-by: herbelin Reviewed-by: ppedrot
2020-09-16More improvements in locating tactic errors.Hugo Herbelin
We finally pass the location in the "ist", and keep it in the "VFun" which is associated to expanded Ltac constants.
2020-09-15A temporary fix of #13018 and #12775 for branch 8.2.Hugo Herbelin
We arbitrarily use max_int as higher level of custom entries in printing, which should be ok since only < and <= are used to decide when to use coercions.
2020-09-15Updated .csdp.cache.test-suite and minor fixesBESSON Frederic
- merlin.in : added zarith - test-suite/Makefile remove .csdp.cache on make clean updated .csdp.cache.test-suite
2020-09-15[micromega] [test-suite] Update csdp cache for num -> zarith migrationEmilio Jesus Gallego Arias
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
Keep Numeral Notation wit a deprecation warning.
2020-09-10Use fresher names in eqschemes.Jasper Hugunin
The previous implementation appears to be sound when Mangle Names is off, but it relies on two fragile assumptions, namely that next_global_ident_away always returns different identifiers when called with naming hints which are different after stripping all digits from the end, and that default_id_of_sort (locally defined) never returns "HC" or "P", or either of those followed by a string of digits. These changes make both assumptions unnecessary. As a side note, it seems odd that fresh is ignoring it's env parameter.
2020-09-10When a notation is only parsing, do not attach to it a specific format.Hugo Herbelin
2020-09-09Merge PR #7825: [tactics] Refine test for unresolved evars: not reachable ↵Pierre-Marie Pédrot
from initial evars Ack-by: JasonGross Ack-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: gares Ack-by: jfehrle Ack-by: maximedenes Reviewed-by: ppedrot
2020-09-08Merge PR #12931: Proof using cleanup, small doc addition and fix using Type ↵coqbot-app[bot]
in collections Reviewed-by: gares Ack-by: Zimmi48
2020-09-08Merge PR #12954: Fixes a freshness issue with destruct/induction (see ↵Pierre-Marie Pédrot
comment in #12944). Ack-by: RalfJung Ack-by: jashug Reviewed-by: ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 02:10:17 +0000