| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
We seized this opportunity to do a little refreshing of the section
describing injection.
|
| |\ |
|
| |\ \ |
|
| | | | |
|
| | | | |
|
| |\ \ \ |
|
| | |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This commits documents the as clause of specialize and that the
as clause of pose proof is optional.
It also mentions a feature of assert ( := ) that was available
since 8.5 and was mentionned by @herbelin in:
https://github.com/coq/coq/pull/248#issuecomment-297970503
|
| |\ \ \ |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
let-ins
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | | |
As per Enrico's request.
|
| | |_|/ /
|/| | | |
|
| | | | | |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
record fields.
|
| | | | | | |
|
| | | | | | |
|
| | |_|/ /
|/| | |
| | | |
| | | | |
Since About mentions it the doc should as well.
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
off by default
|
| | |_|/ /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
- Supporting let-ins in tactic "fix", and hence in interactive
Fixpoint and mutual theorems.
- Documenting more precisely the meaning of n in tactic "fix id n".
- Fixing computation of recursive index at interpretation time in the
presence of let-ins.
|
| |\ \ \ \ |
|
| | | | | | |
|
| | |/ / /
|/| | | |
|
| |\ \ \ \ |
|
| | |_|/ /
|/| | |
| | | |
| | | |
| | | | |
And an extra minor changes (use of zeroone when relevant, use of type
rather than term).
|
| |\ \ \ \ |
|
| | | | | | |
|
| |\ \ \ \ \ |
|
| | |_|_|/ /
|/| | | | |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Maxime points out that -notop cannot be used as the kernel requires
all constants to belong into a module. Indeed:
```
$ rlwrap ./bin/coqtop -notop
Coq < Definition foo := True.
Toplevel input, characters 0-23:
> Definition foo := True.
> ^^^^^^^^^^^^^^^^^^^^^^^
Error: No session module started (use -top dir)
Coq < Module M. Definition foo := True. End M.
Module M is defined
Coq < Locate foo.
Constant If you see this, it's a bug.M.foo
(shorter name to refer to it in current context is M.foo)
```
My rationale for the removal is that this kind of incomplete features
are often confusing to newcomers ─ it has happened to me many times ─
as it can be seen for example in #397 .
|
| |\ \ \ \ \
| |/ / / /
|/| | | | |
|
| | | | | | |
|
| | |/ / /
|/| | | |
|
| | |/ /
|/| |
| | |
| | |
| | | |
This commit removes from the source tree plugins/decl_mode,
its chapter in the reference manual and related tests.
|
| |/ / |
|
| |\| |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | | |
|
| | | |
|
| | | |
|
| |\ \ |
|
| | |/ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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
|
| | | |
|
Hugo Herbelin
Maxime Dénès
Pierre-Marie Pédrot
Jason Gross
Pierre Courtieu
Théo Zimmermann
Paul Steckler
Jason Gross
Gaetan Gilbert
Guillaume Melquiond
Valentin Robert
Emilio Jesus Gallego Arias
Enrico Tassi
Théo Zimmermann
Matthieu Sozeau