| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This made the whole pp code complicated only for the purpose of the
beautifier, while it is not clear when this was useful.
Removing the code for simplicity, not excluding to later address
beautifier issues when they show up.
|
|
This was for the translator and is not relevant for the beautifier.
|
|
|
|
|
|
The option can be turned on by the user though.
|
|
|
|
Note that this is still broken when loading files containing C-zar scripts.
|
|
|
|
... in pose proof of large proof terms
|
|
|
|
We simply remove the warnings about paths mixing Win32 and Unix
separators, since that situation does not seem problematic (c.f.
discussion on the bug tracker).
|
|
Was PR#335: Fix printing of typeclasses eauto debug wrt intro.
|
|
Was PR#336: Remove v62
|
|
|
|
Some options are expected to be deprecated
|
|
This was not detected by running coq-contribs, so it probably means that
we are not testing with the right version of OCaml.
|
|
Was PR#340: Fix various shortcomings of the warnings infrastructure.
|
|
|
|
This commit makes the traversing strategy of typeclasses
eauto an optional argument of the function that implements
it.
This change should be non-breaking.
|
|
be the instance writer's responsibility to not generated non-dependent
non-class subgoals (otherwise we loose compatibility as shown in
e.g. MathClasses, which goes into loops because of unexpectedly
unconstrained goals). Reflect it in the doc.
|
|
- One was expecting shelved goals to remain after resolution (from refine).
- The other too were relying on the wrong classification of subgoals
as typeclass subgoals at toplevel.
|
|
|
|
Now [typeclasses eauto] mimicks what happens during resolution
faithfully, and the shelving behavior/requirements for a successful
proof-search are documented.
|
|
This was the source of a bug in #5115#c7.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
In addition to a priority, cleanup the interfaces for passing this
information as well. The pattern, if given, takes priority over the
inferred one.
We only allow Existing Instances gr ... gr | pri. for now, without
pattern, as before.
Make the API compatible to 8.5 as well.
|
|
With update after J. Gross comments
|
|
This reverts commit 5358515f23d1cd47d4914c55dcf049df858b9dc7.
The syntax is deprecated in 8.6, so we now remove it from trunk.
|
|
|
|
Was PR#341: Better Arguments compatibility.
|
|
|
|
With multiple arguments list, repeating the "/" modifier used to be
mandatory. So instead of forbidding it, we issue a deprecation warning.
|
|
- The flags are now interpreted from left to right, without any other
precedence rule. The previous one did not make much sense in interactive
mode.
- Set Warnings and Set Warnings Append are now synonyms, and have the
"append" semantics, which is the most natural one for warnings.
- Warnings on unknown warnings are now printed only once (previously the
would be repeated on further calls to Set Warnings, sections closing,
module requiring...).
- Warning status strings are normalized, so that e.g. "+foo,-foo" is reduced
to "-foo" (if foo exists, "" otherwise).
|
|
This is a better (more generic) fix to #5061 than my e8b9ee76.
|
|
Strangely enough, the checker seems to rely on an outdated decompose_app
function which is not the same as the kernel, as the latter is sensitive
to casts. Cast-manipulating functions from the kernel are only used on
upper layers, and thus was moved there.
|
|
We return an option type, as constraints were always dropped if the boolean
was false. They did not make much sense anyway.
|
|
|
|
Before this patch, this module was a member of the library folder, which had
little to do with its actual use. A tiny part relative to global registering
of universe names has been effectively moved to the Global module.
|
