| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| |\ \ |
|
| | | | |
|
| | | |
| | |
| | |
| | | |
This is a test for commit 9d1230d484a2cf519f9cd76dc0f37815f3c6339b.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We use heaps instead of continuously adding elements to an ordered list,
which was quadratic in the worst case.
As a byproduct, this solves bug #5359, which was due to a stack overflow on
big lists.
|
| |\ \ \
| | |/
| |/| |
|
| | |\ \
| | | |
| | | |
| | | | |
printer.
|
| | |\ \ \ |
|
| | | |/ /
| |/| |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We solve https://coq.inria.fr/bugs/show_bug.cgi?id=4789 by printing
all the errors from the feedback handler, even in the case of coqtop.
All error display is handled by a single, uniform path.
There may be some minor discrepancies with 8.6 as we are uniform now
whereas 8.6 tended to print errors in several ways, but our behavior
is a subset of the 8.6 behavior.
We had to make a choice for `-emacs` error output, which used to vary
too. We have chosen to display error messages as:
```
(location info) option \n
(program caret) option \n
MARKER[254]Error: msgMARKER[255]
```
This commit also fixes:
- https://coq.inria.fr/bugs/show_bug.cgi?id=5418
- https://coq.inria.fr/bugs/show_bug.cgi?id=5429
|
| | | |/
| |/| |
|
| |\| | |
|
| | |\ \ |
|
| | | | | |
|
| | |\ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Bug #4957 was "unify cannot directly unify universes with evars, but can
do so indirectly".
|
| | |\ \ \ \
| | | |/ /
| | |/| | |
|
| | | | | | |
|
| |\| | | | |
|
| | | |/ /
| |/| |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Also adding spaces around ":=" and ":" when printed as "(x : t := c)".
Example:
Check fun y => let x : True := I in fun z => z+y=0.
(* λ (y : nat) (x : True := I) (z : nat), z + y = 0
: nat → nat → Prop *)
|
| | |\| | |
|
| | | |\ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Fixes Coq bug 5345 (https://coq.inria.fr/bugs/show_bug.cgi?id=5345):
Cannot use names bound in matches inside Ltac definitions.
|
| | |\| | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
That way, (IZR 5) is no longer reduced to 2 + 1 + 1 + 1 (which is not
convertible to 5) but instead to 1 + 2 * 2 (which is). Moreover, it means
that, after reduction, real constants no longer exponentially blow up.
Note that I was not able to fix the test-suite for the declarative mode,
so the missing proof terms have been admitted.
|
| | | |/ /
| | | |
| | | |
| | | |
| | | |
| | | | |
Fixes [Coq bug #5372](https://coq.inria.fr/bugs/show_bug.cgi?id=5372)
"Anomaly: Not a valid information when defining mutual fixpoints that
are not mutual with Function".
|
| | |\| | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Previously to this patch, Coq featured to distinct logging paths: the
console legacy one, based on `Pp.std_ppcmds` and Ocaml's `Format`
module, and the `Feedback` one, intended to encapsulate message inside a
more general, GUI-based feedback protocol.
This patch removes the legacy logging path and makes feedback
canonical. Thus, the core of Coq has no dependency on console code
anymore.
Additionally, this patch resolves the duplication of "document" formats
present in the same situation. The original console-based printing code
relied on an opaque datatype `std_ppcmds`, (mostly a reification of
`Format`'s format strings) that could be then rendered to the console.
However, the feedback path couldn't reuse this type due to its opaque
nature. The first versions just embedded rending of `std_ppcmds` to a
string, however in 8.5 a new "rich printing" type, `Richpp.richpp` was
introduced.
The idea for this type was to be serializable, however it brought
several problems: it didn't have proper document manipulation
operations, its format was overly verbose and didn't preserve the full
layout, and it still relied on `Format` for generation, making
client-side rendering difficult.
We thus follow the plan outlined in CEP#9, that is to say, we take a
public and refactored version of `std_ppcmds` as the canonical "document
type", and move feedback to be over there. The toplevel now is
implemented as a feedback listener and has ownership of the console.
`richpp` is now IDE-specific, and only used for legacy rendering. It
could go away in future versions. `std_ppcmds` carries strictly more
information and is friendlier to client-side rendering and display
control.
Thus, the new panorama is:
- `Feedback` has become a very module for event dispatching.
- `Pp` contains a target-independent box-based document format.
It also contains the `Format`-based renderer.
- All console access lives in `toplevel`, with console handlers private
to coqtop.
_NOTE_: After this patch, many printing parameters such as printing
width or depth should be set client-side. This works better IMO,
clients don't need to notify Coq about resizing anywmore. Indeed, for
box-based capable backends such as HTML or LaTeX, the UI can directly
render and let the engine perform the word breaking work.
_NOTE_: Many messages could benefit from new features of the output
format, however we have chosen not to alter them to preserve output.
A Future commits will move console tag handling in `Pp_style` to
`toplevel/`, where it logically belongs.
The only change with regards to printing is that the "Error:" header was
added to console output in several different positions, we have removed
some of this duplication, now error messages should be a bit more
consistent.
|
| | | |\ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Augments "A fully applied tactic is expected" with the list of missing
arguments to the tactic. Addresses [bug
5344](https://coq.inria.fr/bugs/show_bug.cgi?id=5344).
|
| | | |\ \ \
| | | | | |
| | | | | |
| | | | | | |
correctly as…
|
| | | |_|_|/
| |/| | |
| | | | |
| | | | |
| | | | | |
This commit removes from the source tree plugins/decl_mode,
its chapter in the reference manual and related tests.
|
| | |\ \ \ \
| | | | | |
| | | | | |
| | | | | | |
Tactic Notation
|
| | |\ \ \ \ \
| | | |/ / /
| | |/| | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This is cumbersome, because now code may fail at link time if it's not
referring to the correct module name. Therefore, one has to add corresponding
open statements a the top of every file depending on a Ltac module. This
includes seemingly unrelated files that use EXTEND statements.
|
| | | | | | | |
|
| | | | |_|/
| | |/| | |
|
| |\| | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Interpretation of patterns in Ltac is essentially flawed. It does a roundtrip
through the pretyper, and relies on suspicious flagging of evars in the evar source
field to recognize original pattern holes. After the pattern_of_constr function
was made evar-insensitive, it expanded evars that were solved by magical side-effects
of the pretyper, even if it hadn't been asked to perform any heuristics.
We backtrack on the insensitivity of the pattern_of_constr function. This may have
a performance penalty in other dubious code, e.g. hints. In the long run we should
get rid of the pattern_of_constr function.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Incidentally, this fixes a printing bug in output/inference.v where the
displayed name of an evar was the wrong one because its type was not
evar-expanded enough.
|
| | |\ \ \ \ |
|
| | |/ / / /
|/| | | |
| | | | |
| | | | |
| | | | | |
Fix the ordering of the results in the output of Search to correspond
to the "priority" ordering.
|
| | | | | | |
|
| | | |/ /
| |/| |
| | | |
| | | | |
In particular, this closes bug 2417.
|
| | |\| | |
|
| | | |\ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This was introduced in 8.5 while reorganizing the structure of
intro-patterns.
|
| | | |\| | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Tracking conversion problems to reconsider was lost for evars subject
to restriction (field last_mods was not updated and conversion
problems not considered to be changed).
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
A cleaning done in ade2363e35 (Dec 2015) was hinting at bugs in typing
a matching over a "catch-all" variable, when let-ins occur in the
arity. However ade2363e35 failed to understand what was the correct
fix, introducing instead the regressions mentioned in #5322 and #5324.
This fixes all of #5322 and #5324, as well as the handling of let-ins
in the arity.
Thanks to Jason for helping in diagnosing the problem.
|
| | | | | | |
|
Maxime Dénès
Pierre-Marie Pédrot
Emilio Jesus Gallego Arias
Gaetan Gilbert
Tej Chajed
Hugo Herbelin
Guillaume Melquiond
Enrico Tassi
Ralf Jung
Arnaud Spiwack
Théo Zimmermann