| Age | Commit message (Collapse) | Author |
|---|
|
work better on them
|
|
A trick in counting spaces in a format was making the empty notation
not behaving correctly.
|
|
When a proper notation variable occurred only in a recursive pattern
of the notation, the notation was wrongly considered non printable due
(the side effect that function compare_glob_constr and that
mk_glob_constr_eq does not do anymore was indeed done by aux' but
thrown away). This fixes it.
|
|
The two previous commits make the warning irrelevant and useless.
|
|
- Formerly, notations such as "{ A } + { B }" were typically split
into "{ _ }" and "_ + _". We keep the split only for parsing, which
is where it is really needed, but not anymore for interpretation,
nor printing.
- As a consequence, one notation string can give rise to several
grammar entries, but still only one printing entry.
- As another consequence, "{ A } + { B }" and "A + { B }" must be
reserved to be used, which is after all the natural expectation,
even if the sublevels are constrained.
- We also now keep the information "is ident", "is binder" in the
"key" characterizing the level of a notation.
|
|
|
|
Fixes bug 5597.
|
|
y , z".
|
|
|
|
Since camlp5 parses from left, the last ", z" was parsed as part of an
arbitrary long list of "x1 , .. , xn" and a syntax error was raised
since an extra ", z" was still expected.
We support this by translating "x , .. , y , z" into "x , y , .. , z"
and reassembling the arguments appropriately after parsing.
|
|
|
|
eval thunks once in prlist_sep_lastsep, make code clearer
add typeclass debug output test
|
|
|
|
constant".
|
|
Delaying also some computation needed for printing to the time of
really printing it.
|
|
|
|
|
|
|
|
The user now has to manually load them, respectively via:
Require Extraction
Require Import FunInd
The "Import" in the case of FunInd is to ensure that the
tactics functional induction and functional inversion are indeed
in scope.
Note that the Recdef.v file is still there as well (it contains
complements used when doing Function with measures), and it also
triggers a load of FunInd.v.
This change is correctly documented in the refman, and the test-suite
has been adapted.
|
|
See now https://github.com/coq/bignums
Int31 is still in the stdlib.
Some proofs there has be adapted to avoid the need for BigNumPrelude.
|
|
|
|
Also taking into account a name in the return clause and in the
indices.
Note the double meaning ``bound as a term to match'' and ``binding in
the "as" clause'' when the term to match is a variable for all of
"match", "if" and "let".
|
|
|
|
|
|
We remove the emacs-specific printing code from the core of Coq, now
`-emacs` is a printing flag controlled by the toplevel.
|
|
recursive notations) (bis)
|
|
This was preventing to work examples such as:
Notation "[ x ; .. ; y ; z ]" := ((x,((fun u => u), .. (y,(fun u =>u,z)) ..))).
|
|
This allows a better control on the name to give to an evar and, in
particular, to address the issue about naming produced by "epose
proof" in one of the comment of Zimmi48 at PR #248 (see file names.v).
Incidentally updating output of Show output test (evar numbers shifted).
|
|
|
|
|
|
printing only
|
|
|
|
|
|
with binders)
|
|
|
|
|
|
- https://coq.inria.fr/bugs/show_bug.cgi?id=5529
- https://coq.inria.fr/bugs/show_bug.cgi?id=5537
See also PR #640
|
|
|
|
With the "apply in" introduction pattern, and the backtrack possibly
done in "apply" over the components of conjunctions
(descend_in_conjunctions), the reasons for failing might have
different sources.
We give priority to the detection of used names over other
(unification) errors so that an error there is not masked in the
backtracking made by descend_in_conjunctions.
Of course, the question of what best unification error to give in the
presence of backtracking is still open.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
record fields.
|
|
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.
|
|
|
|
|
|
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
|
