| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
Not sure if worth using in other places.
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This removes the Flags.univ_print in the kernel, making it possible to
put the univ printing flag ownership back in Detyping.
The lazyness is because getting an explanation may be costly and we
may discard it without printing.
See benches
- with lazy
https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/406/console
- without lazy
https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/405/console
Notably without lazy mathcomp odd_order is +1.26% with some lines
showing significant changes, eg PFsection11 line 874 goes from 11.76s
to 13.23s (+12%).
(with lazy the same development has -1% overall and the same line goes
from 11.76s to 11.23s (-4%) which may be within noise range)
|
| |/
|
|
| |
ie don't go through having Eq constraints but directly to the unionfind.
|
| |\ |
|
| | | |
|
| |/ |
|
| |
|
|
|
| |
New module introduced in OCaml 4.05 I think, can create problems when
linking with the OCaml toplevel for `Drop`.
|
| |
|
|
| |
We do up to `Term` which is the main bulk of the changes.
|
| |
|
|
|
|
|
|
| |
We export a function in UGraph to check that a polymorphic instance is
a subtype of another, instead of rolling up our own in module code.
We also add a few tests for module subtyping in presence of polymorphic
constants.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
```
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Universes are kept in normal form w.r.t. equality but not the <=
relation, so the previous check worked almost always but was actually
too strict! In cases like (max(Set,u) = u) when u is declared >= Set it
was failing to find an equality. Applying the KISS principle:
u = v <-> u <= v /\ v <= u.
Fix invariant breakage that triggered the discovery of the check_eq bug as well. No algebraic universes should appear in a term position (on the left of
a colon in a typing judgment), this was not the case when an algebraic
universe instantiated an evar that appeared in the term. We force their
universe variable status to change in refresh_universes to avoid this.
Fix ind sort inference: Use syntactic universe equality for inductive
sort inference instead of check_leq (which now correctly takes
constraints into account) and simplify code
|
| |
|
|
|
|
| |
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
|
|
1. The Univ module now only cares about definitions about universes.
2. The UGraph module contains the algorithm responsible for aciclicity.
|
Gaëtan Gilbert
Pierre-Marie Pédrot
Maxime Dénès
Théo Zimmermann
Emilio Jesus Gallego Arias
Jason Gross
Matthieu Sozeau
Pierre Letouzey
Jacques-Henri Jourdan
Guillaume Melquiond