| Age | Commit message (Collapse) | Author |
|---|
|
|
|
The bug has been solved as a side-effect of the EConstr branch.
|
|
|
|
|
|
|
|
|
|
Add a test-suite file to be sure we won't regress silently.
|
|
To use the generic combinator, we introduce a side effect. I believe
that we have more to gain from a short code than from being purely
functional.
This also fixes the expected semantics since the variables binding the
return type in "match" were not taking into account.
|
|
Binding generalizable_vars_of_glob_constr, occur_glob_constr,
free_glob_vars, and bound_glob_vars on it.
Most of the functions of which it factorizes the code were bugged with
respect to bindings in the return clause of "match" and in either the
types or the bodies of "fix/cofix".
|
|
record fields.
|
|
Also remove obvious comments.
|
|
|
|
|
|
|
|
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.
|
|
in the presence of let-ins.
|
|
This was assuming dependencies occurring in configurations of
the form x:A, y:B x, z:C x y |- match x, y, z with ... end".
But still work to do for better management of dependencies in general...
|
|
This allows e.g. to use the record notations even when there are
defined fields.
A priori fixed also missing parameters when interpreting primitive
tokens.
|
|
|
|
|
|
printer.
|
|
|
|
Was needed to be done for a while.
|
|
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).
|
