| Age | Commit message (Collapse) | Author |
|---|
|
This commit uses the proper url for bug reporting, marks urls as such,
stops qualifying the Coq'Art book as new, and fix the spacing after the
Coq name.
|
|
|
|
The way \zeroone was defined, the \tt modifier was leaked outside the
brackets, thus messing with the following text. There are a bunch of
occurrences of this issue in the manual, so rather than turning all the
\tt into \texttt, the definition of \zeroone is made more robust.
Unfortunately, there is one single occurrence of \zeroone that does not
support the more robust version. (Note that this specific usage of
\zeroone is morally a bug, since it goes against all the LaTeX
conventions.) So the commit also keeps the old leaky version of \zeroone
around as \zeroonelax so that it can be used there.
|
|
|
|
|
|
|
|
Was PR#364: Add missing label. Fixes broken ref.
|
|
|
|
Note: "dependant" does exist, but it is a noun and it means a person that
is somehow financially dependent on someone else.
|
|
|
|
We stop failing automatically on non-declared-class nested or toplevel
subgoals as in 8.5, instead of the previous a477dc behavior of shelving
those goals and failing if shelved goals remained at the end of
resolution. It means typeclass resolution during refinement is closer to
all:typeclasses eauto. Hints in typeclass_instances for non-declared
classes can be used during resolution of _nested_ subgoals when it is
fired from type-inference, toplevel goals considered in this case are
still only classes (as in 8.5 and before). The code that triggers the
restriction to only declared class subgoals is commented.
Revert changes to test-suite, adding test for #5203, #5198 is fixed too.
Add corresponding tests in the test-suite (that will break if we,
e.g. disallow non-class subgoals) and update the refman accordingly.
|
|
In only_classes mode we do not try to implement a stricter semantics for
shelved goals in 8.6. Leaving this for 8.7.
Update the documentation as well.
Remove a spurious printf call as well.
Fix test-suite now that shelved goals are allowed
|
|
|
|
|
|
Was PR#348: Credits for 8.6
|
|
|
|
|
|
|
|
Was PR#339: Documenting type class options, typeclasses eauto
|
|
They allow to call refine without doing typeclass resolution, allowing
to use refine in typeclass hints.
|
|
Command used: git log v8.5..HEAD --pretty=format:"%an," | sort -k 2 | uniq
with some manual postprocessing for login names, particles and multiple first names.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Was PR#336: Remove v62
|
|
|
|
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.
|
|
Now [typeclasses eauto] mimicks what happens during resolution
faithfully, and the shelving behavior/requirements for a successful
proof-search are documented.
|
|
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
|
|
|
|
|
|
|
|
These variants are from 8.3 but were never documented except in CHANGES.
|
|
The doc of auto hints now mention again that sometimes a hint
will be used with simple apply and sometimes it will be used
with exact.
It does not try to be fully precise in that we don't
necessarily want to document the behaviors of auto that
we might like to change.
See also the discussion on commit 9227d6e.
|
|
This way of giving the summary avoids redundancy as much as possible.
It is helpful for the auto-completion of Company-Coq of @cpitclaudel.
|
|
Now that this tactic has been fixed (commit 58d1381),
it needed to get documented.
|
|
Improve the description of what auto/eauto do.
These two tactics rely on the simple version of apply/eapply.
Since this simple version is available to the end user,
it is better to mention it. See also the confusion that such
description can create in the thread "Understanding auto" on Coq-Club.
|
|
between proofs in tactic injection, with a side-effect on inversion.
|
|
Was PR#280: Document that [Reset Ltac Profile] is not synchronized with
the document state
|
|
|
|
Was PR#232: Fix the parsing of goal selectors.
|
|
|
|
|
|
as suggested by Hugo. Also, escape the spaces after the dots to obtain
a better PdfLaTeX output.
|
|
- Ensure "coq_makefile --help" is properly typeset with HeVeA/PdfLaTeX
- Replace 's with "s so they are typeset as true ASCII characters
- Add missing ; before closing brace.
|
|
|
