aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Collapse)Author
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-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-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-11Rename Numeral Notation command to Number NotationPierre Roux
Keep Numeral Notation wit a deprecation warning.
2020-09-03Fix incorrect debruijn handling when Record calls maybe_unify_params_inGaëtan Gilbert
Fix #12887
2020-09-02Fixes #9403 and #10803 (missing flattening of nested applications in notations).Hugo Herbelin
The bugs involved: - a notation with a subterm in position of function of an application - use of this notation in another notation creating a non-flattened application In particular, this fooled "find_appl_head" (for #10803) and the translation from GApp to NApp (for #9403). We fix the translation NApp -> GApp (since glob_constr is supposed to have its applications flattened).
2020-08-31Merge PR #12875: Further extensions of About wrt Arguments and renamingcoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: herbelin
2020-08-28About: Add a mention that arguments have been renamed, if ever it is the case.Hugo Herbelin
See https://github.com/coq/coq/pull/12875#issuecomment-679190489.
2020-08-28Where there are several lists of implicit arguments, don't pretend names matter.Hugo Herbelin
That is, in "About", use _ for the variables of the extra lists. See discussion at https://github.com/coq/coq/pull/12875#issuecomment-679190489.
2020-08-28Do not write "rename" for arguments in About, since these arguments are ↵Hugo Herbelin
validated.
2020-08-28When printing the type in About, use the renamed arguments.Hugo Herbelin
2020-08-28When reporting an implicit argument error on a rename argument, use the ↵Hugo Herbelin
renaming. Example: > Arguments id [B] {b} : rename. > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: Argument B is a trailing implicit, so it can't be declared non maximal. Please use { } instead of [ ].
2020-08-28In "About", print all arguments, even if it is trailing list of _.Hugo Herbelin
2020-08-28par: print relevant subgoal when failingGaëtan Gilbert
Fix (partial) #5502
2020-08-27Merge PR #12877: Propagate in-context information for explicitation of extra ↵coqbot-app[bot]
arguments of notations Reviewed-by: SkySkimmer Ack-by: herbelin
2020-08-25Merge PR #12897: [test-suite] close the proof added in #12857coqbot-app[bot]
Reviewed-by: Zimmi48
2020-08-25The body of a let is considered to be "in context" if its type is present.Hugo Herbelin
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-08-25Merge PR #12758: Fixing a coercion entry transitivity bug.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-08-25[test-suite] close the proofEnrico Tassi
2020-08-25Propagate in-context information for extra arguments of notations too.Hugo Herbelin
2020-08-21Merge PR #12853: Another tactic error location fix after PR#12223 and PR#12774Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-08-21Merge PR #12857: [ssr] when porting v8.2 code no backtracking point has to ↵Pierre-Marie Pédrot
be added Reviewed-by: CohenCyril Reviewed-by: ppedrot
2020-08-21Merge PR #12759: [vernac] refine check for unresolved evarscoqbot
Reviewed-by: SkySkimmer Ack-by: gares
2020-08-20[ssr] when porting v8.2 code no backtracking point has to be addedEnrico Tassi
Amends c1b1afe76e1655cc3275bdf4215f0ab690efc3cc
2020-08-20Merge PR #12756: Do not refresh the names of implicit arguments.Maxime Dénès
Reviewed-by: herbelin Reviewed-by: maximedenes
2020-08-20[vernac] refine check for unresolved evarsEnrico Tassi
2020-08-19Yet other tactic error location fixes (see PR#12223 and PR#12774).Hugo Herbelin
When calling an Ltac function, add specific locations when interpreting the function, when interpreting the arguments and when executating the call (in a TacArg).
2020-08-19Do not refresh the names of implicit arguments.Jasper Hugunin
Try just going with the user-given names, and not worrying about what happens with repeated names or anonymous implicits. (Support for anonymous implicits is due to herbelin in #11098.) This PR should not change behaviour in the absence of repeated names. Since repeated names are already a poorly handled corner case, I would recommend changing binder names to avoid overlap in the case of a change in behavior. Since anonymous implicits and implicits with repeated names can already happen, I think this is unlikely to cause too many new problems, though it might exacerbate existing ones. However, I already had to fix one newly possible anomaly, so I can't be too confident. The most common change in external developments was that an argument no longer gets `0` appended to it, causing the `Arguments` command to complain about renaming. To fix this and keep the old name, one can simply use the `rename` flag as suggested, or switch to the new, un-suffixed name. Closes #6785 Closes #12001 Another step towards checking the standard library with `-mangle-names`.
2020-08-18Remaining bugs in PR#12223 which fixed location of tactic errors (issue #12152).Hugo Herbelin
The update of a loc needs sometimes to override (when calling an Ltac function), and otherwise to keep the existing loc (assumed to be fined). We refine this (see e.g. the ErrorLocation_tac_in_term tests). Moreover, when overriding, this was going to a tclOR backtracking point which was setting the loc to a completely disjoint part of the code having caused the error (see #12773). We replace the tclOR by a tclORELSE.
2020-08-09Fixing a coercion entry transitivity bug.Hugo Herbelin
2020-07-21Merge PR #12697: Fix bug #12691: an only-parsing notation needs to produce a ↵Emilio Jesus Gallego Arias
generic printing format in anticipation of further not-only-parsing uses of the notation Reviewed-by: ppedrot
2020-07-20Merge PR #12684: Do not print constructor and inductive types as terms when ↵Gaëtan Gilbert
asked to be printed as themselves Reviewed-by: SkySkimmer
2020-07-15Do not print global refs as terms when asked to be printed as themselves.Hugo Herbelin
This was already the case for constant, but not for constructors and inductive types. For instance, in message "The constructor @cons (in type list) is expected to ..." we don't want a @ to be printed.
2020-07-15Fix bug #12691 (an only parsing notation induces a generic printing format).Hugo Herbelin
This is to anticipate further not-only-parsing uses of the notation.
2020-07-12Fixes #12682 (recursive notation printing bug with n-ary applications).Hugo Herbelin
A special case for recursive n-ary applications was missing when the head of the application was a reference.
2020-07-08Adding test for #12525 (Search of lemmas in Include failing when in Module).Hugo Herbelin
2020-07-01UIP in SPropGaëtan Gilbert
2020-06-25Generate names for anonymous polymorphic universesGaëtan Gilbert
This should make the univbinders output test less fragile as it depends less on the global counter (still used for universes from section variables).
2020-06-22Merge PR #12434: Slight improvement in naming dependent existential ↵Gaëtan Gilbert
variables in goals Reviewed-by: SkySkimmer
2020-06-11Merge PR #12443: Fix #12442: Confusing error message when the intro pattern ↵Pierre-Marie Pédrot
of "apply in" fails Reviewed-by: ppedrot
2020-06-11Merge PR #12423: Remove info tactic, deprecated in 8.5Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-06-09Merge PR #12186: CReal: changed epsilon for modulus of convergence from 1/n ↵Vincent Semeria
to 1/2^n Reviewed-by: VincentSe
2020-06-09CReal: changed epsilon for modulus of convergence from 1/n to 2^zMichael Soegtrop
2020-06-08Don't suggest Proof using when no section variablesGaëtan Gilbert
Fix #12447
2020-06-06Fix #12442: Confusing error message when the intro pattern of "apply in" failsAttila Gáspár
2020-06-01Slight improvement in naming existential variables.Hugo Herbelin
In a Meta := Evar unification problem and the Meta is bound to a (named) binder, and the Evar is a GoalEvar, we set the source of the evar to be the one of the Meta.
2020-05-30Remove info tactic, deprecated in 8.5Jim Fehrle
2020-05-25Fix output tests for location errors when running in async mode.Théo Zimmermann
In this mode, an additional error was emitted, which made the test fail: Error: There are pending proofs: Unnamed_thm.
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-11 11:35:09 +0000