| Commit message (Collapse) | Author | Age |
|---|
| |\
| |
| |
| | |
constructs.
|
| | |
| |
| |
| |
| |
| | |
Extending terms is notoriously difficult. We try to get more help from
the compiler by making sure such an extension will trigger non
exhaustive pattern matching warnings.
|
| |/
|
|
|
|
| |
We deprecate a few functions that were deprecated in the comments plus
we place `Nameops` and `Univops` in engine where they do seem to
belong in the large picture of code organization.
|
| |\ |
|
| | |
| |
| |
| | |
We do up to `Term` which is the main bulk of the changes.
|
| |/
|
|
| |
Fixes #6022.
|
| |
|
|
|
| |
Compared to the original proposition (01f848d in #960), this commit
only changes files containing bug numbers that are also PR numbers.
|
| |\
| |
| |
| | |
Compute plugin
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
BZ#4852)
This code simplification isn't that important, but it can trigger further
simplifications elsewhere, see for instance BZ#4852.
NB: normally, the extraction favors eta-expanded forms, since that's the usual
way to avoid issues about '_a type variables that cannot be generalized. But
the atomic eta-reductions done here shouldn't be problematic (no applications
put outside of functions).
|
| |/
|
|
| |
See https://github.com/letouzey/extraction-compute for more details
|
| |
|
|
|
| |
The old algorithm was relying on list membership, which is O(n). This was
nefarious for terms with many binders. We use instead sets in O(log n).
|
| |\
| |
| |
| | |
work better on them
|
| | |
| |
| |
| |
| |
| |
| |
| | |
As explained in edf85b9, the original commit that merged the module_body
and module_type_body representations, this was delayed to a later time
assumedly due to OCaml lack of GADTs. Actually, the only thing that was
needed was polymorphic recursion, which has been around already for a
relatively long time (since 3.12).
|
| |/ |
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| | | | | |
|
| | |_|/
|/| | |
|
| |\ \ \
| |_|/
|/| |
| | | |
4844 and 4824)
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The use of template polymorphism in constants was quite limited, as it
only applied to definitions that were exactly inductive types without any
parameter whatsoever. Furthermore, it seems that following the introduction
of polymorphic definitions, the code path enforced regular polymorphism as
soon as the type of a definition was given, which was in practice almost
always.
Removing this feature had no observable effect neither on the test-suite,
nor on any development that we monitor on Travis. I believe it is safe to
assume it was nowadays useless.
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | |_|/ /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This ensures that the API is self-contained and is, well, an API.
Before this patch, the contents of `API.mli` bore little relation with
what was used by the plugins [example: `Metasyntax` in tacentries.ml].
Many missing types had to be added.
A sanity check of the `API.mli` file can be done with:
`ocamlfind ocamlc -rectypes -package camlp5 -I lib API/API.mli`
|
| | |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
4844 and 4824)
The commit 8e257d4 (which consider the dummy type Tdummy to be polymorphic and hence
immune of the need for unsafeCoerce) is quite wrong, even if in pratice it worked ok
most of the time. The confusion comes from the fact that the dummy value (__ aka MLdummy
internally) is implemented in Haskell as Prelude.error, hence it has indeed a polymorphic
unrestricted type. But the dummy type Tdummy used when extracting types must be monomorphic
(otherwise type parameters would have to be propagated out of any type definition involving
Tdummy). We implement Tdummy by Haskell's (), which for instance isn't convertible to Any,
as shown by the examples in bug reports 4844 and 4824.
This fix will bring back some more unsafeCoerce in Haskell extraction, including possibly
a few spurious ones. And these extra unsafeCoerce might also hinder further code optimisations.
We tried to mitigate that by directly removing [MLmagic] constructors in front of [MLdummy _].
NB: even if the original bug report mentions universe polymorphism, this issue is
almost unrelated to it. It just happens that when universe polymorphism is off,
an inductive instance is fully placed in Prop (cf. template polymorphism) in the example,
avoiding triggering the issue.
Warning: the test-suite file is there for archiving the repro case, but currently it doesn't
test much (we should run ghc on the extracted code).
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Avoid Anomaly (or Assert False) when a module signature contains
an applied functor followed by a "with Definition" or "with Module"
Also fix the dependency computation in presence of a "with Definition"
Concerning 4720, the code extracted out of this bug report was suboptimal
in Coq 8.4 (it was compilable, but could have probably been tweaked into a
real issue producing faulty code).
But the example of 4720 (and some variants of it) was broken since 8.5,
for the same reasons as 5177 and 5240. And the good news is that after
these repairs, the example of bug 4720 is now extracted to correct code
(the "with" is preserved).
|
| | | |
|
| | | |
|
| |/
|
|
|
|
|
|
|
|
|
|
|
| |
Extraction TestCompile foo
is equivalent to:
Extraction "/tmp/testextraction1234.ml" foo
ocamlfind ocamlc -I /tmp -c /tmp/testextraction1234.mli /tmp/testextraction1234.ml
This command isn't meant for the end user, but rather as an helper
for test-suite scripts. It only works with extraction to OCaml,
and the generated code should be standalone.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |\ |
|
| | | |
|
| |/ |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
As per https://github.com/coq/coq/pull/716#issuecomment-305140839
Partially using
```bash
git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i
```
and
```bash
git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i
```
The rest were manually edited by looking at the results of
```bash
git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less
```
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
Deprecations which can't be fixed in 4.02.3 are locally wrapped with
[@@@ocaml.warning "-3"]. The only ones encountered are
- capitalize to capitalize_ascii and variants. Changing to ascii would
break coqdoc -latin1 and maybe other things though.
- external "noalloc" to external [@@noalloc]
|
| |/
|
|
|
|
|
|
|
|
|
|
|
| |
This is the continuation of #244, we now deprecate `CErrors.error`,
the single entry point in Coq is `user_err`.
The rationale is to allow for easier grepping, and to ease a future
cleanup of error messages. In particular, we would like to
systematically classify all error messages raised by Coq and be sure
they are properly documented.
We restore the two functions removed in #244 to improve compatibility,
but mark them deprecated.
|
| |\ |
|
| |\ \ |
|
| | |/
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which
this PR solves, I propose to remove support for non-synchronous
options.
It seems the few uses of `optsync = false` we legacy and shouldn't
have any impact.
Moreover, non synchronous options may create particularly tricky
situations as for instance, they won't be propagated to workers.
|
| | | |
|
| |/
|
|
|
|
|
|
|
|
|
|
| |
This completes the Loc.ghost removal, the idea is to gear the API
towards optional, but uniform, location handling.
We don't print <unknown> anymore in the case there is no location.
This is what the test suite expects.
The old printing logic for located items was a bit inconsistent as
it sometimes printed <unknown> and other times it printed nothing as
the caller checked for `is_ghost` upstream.
|
| |\ |
|
| | |
| |
| |
| |
| | |
This reverts commit 6d2802075606dcddb02dd13cbaf38ff76f8bf242, which is
an 8.6 only commit.
|
| | |\ |
|
| | | |
| | |
| | |
| | |
| | | |
This way, after we merge PR#220, scripts can be fixed in a way that is
compatible with the 8.6 and trunk branches.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Previous implementations of `Pp` flushed on newline, however,
depending on the formatter this may not be always the case.
We now alwayas flush the formatters before closing the file as this is
the intended behavior.
|
Maxime Dénès
Emilio Jesus Gallego Arias
Tej Chajed
Théo Zimmermann
Pierre Letouzey
Pierre-Marie Pédrot
Hugo Herbelin
Matej Košík
Jason Gross
Gaëtan Gilbert