| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | |_|_|_|/ / /
|/| | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
This changes the implementation of "constructor" from
constructor 1 + ... + constructor n + fail
to
constructor 1 + ... + constructor n.
|
| | | | | | | | |
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
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.
|
| | |_|_|_|/ /
|/| | | | |
| | | | | |
| | | | | | |
For instance, we don't want "id@{u}" to be coerced to id, or "?[n]" to "_".
|
| |\ \ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
artificially restricted to a non-empty context).
|
| |\ \ \ \ \ \ \ |
|
| | | | | | | | | |
|
| | |/ / / / / /
|/| | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
As explained in BZ#5713 report, the requirement for a non-empty
context is not needed, so we remove it.
|
| |\ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
The fix covers the case of a non-dependent goal with unavailable
dependent case analysis: destruct was not seeing that it could still
use non-dependent case analysis.
|
| | | | | | | | | | | | | |
|
| | | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
This is a temporary workaround, until we fix the underlying issue which
makes coqtop hang on those tests.
|
| | | | | | | | | | | | | |
|
| | |_|_|_|/ / / / / / /
|/| | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
The code generating the projection was unconditionally generating
pattern-matchings, although this is incorrect for primitive records.
|
| |\ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
restructuration
|
| |\ \ \ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|/ / / / / / / / / /
|/| | | | | | | | | | | | |
|
| | | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
CAMLPKGS is now used to hold extra findlib -packages
The previous solution was to use CAMLFLAGS but since 4.05 an
invocation of `ocamlopt -pack useless.cmxa foo.cmx -o packedfoo.cmx`
fails saying that `useless.cmxa` is not a compilation unit description.
CAMLPKGS is used in all `ocamlopt` invocations but for the one
performing the packing.
|
| | |_|_|/ / / / / / / / /
|/| | | | | | | | | | | |
|
| | | | | | | | |_|/ / /
| | | | | | |/| | | |
| | | | | | | | | | |
| | | | | | | | | | | |
Fixes BZ#5700
|
| | | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
The two previous commits make the warning irrelevant and useless.
|
| | | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
This reverts commit 53a50875 and a bit more: it also makes the check
for possibly ignoring formatting spaces irrelevant, since the previous
commit makes that curly brackets are not any more dropped for
printing.
|
| | | | | |_|/ / / / /
| | | |/| | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
- 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.
|
| | | | |/ / / / / / |
|
| | | | |/ / / / / |
|
| | | | | |/ / /
| | | |/| | | |
|
| | |_|/ / / /
|/| | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
Commit 8f12597 introduced new output tests but these were broken on Windows.
We fix them by using --strip-trailing-cr option of diff, like in other
output tests in the test-suite.
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This one is a continuation of e2a8edaf59 which was βι-normalizing the
hypotheses created by a "match". We forgot to do it for "let" and
"if". This is what this commit is doing.
|
| | |_|_|_|/
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Formerly, mk_refgoals in logic.ml was applying full βι on new Meta-based goals.
We simulate part of this βι-normalization in pose_all_metas_as_evars.
I suspect that we don't βι-normalize goals more than in 8.4 by doing
that, since all Metas would have eventually gone to mk_refgoals, but
difficult to know for sure as there were probably metas turned to
evars (and hence a priori not βι-normalized) even when logic.ml was
used more pervasively.
However, βι-normalizing is a priori a better heuristic than no
βι-normalizing, independently of what it was in 8.4 and before (even
if, ideally, I would personally lean towards preferring a
"chirurgical" substitution with reduction only at the place of
substitution).
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
wrongly tagged as keywords
|
| |\ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | |
|
| | |_|_|/ / / / / /
|/| | | | | | | |
| | | | | | | | |
| | | | | | | | | |
Fixes bug 5597.
|
| | |_|_|_|/ / / /
|/| | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
This is a second try at removing the hooks for the legacy xml export
system which can't currently be tested.
It is also not included in the API, so it should either be included in
it or this PR be applied.
|
| |\ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
y , z".
|
| | | | | | | | | | | | | |
|
| | | | | | | | | | | | | |
|
| | | | | | | | | | | | | |
|
| | | | | | | |_|/ / / /
| | | | | |/| | | | | |
|
Guillaume Melquiond
Hugo Herbelin
Maxime Dénès
Enrico Tassi
Pierre-Marie Pédrot
Tej Chajed
Matthieu Sozeau
Théo Zimmermann
Emilio Jesus Gallego Arias
Amin Timany