| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
| |
We mirror the structure of EConstr and move the destructors from `Term`
to `Constr`.
This is a step towards having a single module for `Constr`.
|
| | |
|
| |
|
|
| |
We do up to `Term` which is the main bulk of the changes.
|
| |
|
|
| |
This is a first step towards some of the solutions proposed in #6008.
|
| |
|
|
| |
4.02.3 has been the minimal OCaml version for a while now.
|
| |
|
|
|
|
|
|
|
|
|
| |
In particular, this fixes #5757 which used restrict_evar to refine the
information on the source of an evar, and which should have set the
"cleared" flag.
Also renaming flag "restricted" since it is not only about "clear".
I guess this is what we want in general, but I did not survey all uses
of restrict_evar so, maybe, this should be refined further.
|
| |
|
|
|
| |
We dont care about the order of the binder map ([map] in the code) so
no need to do tricky things with it.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
Introduce a "+" modifier for universe and constraint declarations to
indicate that these can be extended in the final definition/proof. By
default [Definition f] is equivalent to [Definition f@{+|+}], i.e
universes can be introduced and constraints as well. For [f@{}] or
[f@{i j}], the constraints can be extended, no universe introduced, to
maintain compatibility with existing developments. Use [f@{i j | }] to
indicate that no constraint (nor universe) can be introduced. These
kind of definitions could benefit from asynchronous processing.
Declarations of universe binders and constraints also works for
monomorphic definitions.
|
| |\ |
|
| | | |
|
| | |\ |
|
| | | | |
|
| | | |
| | |
| | |
| | | |
Use an explicit label ~algebraic for make_flexible_variable as well.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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
```
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We don't want "Anomaly: Returned a functional value in a type not
recognized as a product type.. Please report at
http://coq.inria.fr/bugs/." but instead "Anomaly: Returned a functional
value in a type not recognized as a product type. Please report at
http://coq.inria.fr/bugs/."
|
| | |/ |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
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).
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |\ \ |
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| |/ /
| |
| |
| | |
Now it is a private field, locations are optional.
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
All functions where actually called with the second argument of the pending
problem being the current evar map. We simply remove this useless and
error-prone second component.
|
| |\| | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | |\| |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
named in the original term.
Useful at least for debugging, useful to give a better message than
"this placeholder", even if in the loc is known in this case.
|
| |/| |
| |/ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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
|
| | | |
|
| |\| |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| | |
When printing evar constraints, we ensure that every variable from the
rel context has a name.
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
composition operator.
Short story:
This pull-request:
(1) removes the definition of the "right-to-left" function composition operator
(2) adds the definition of the "left-to-right" function composition operator
(3) rewrites the code relying on "right-to-left" function composition to rely on "left-to-right" function composition operator instead.
Long story:
In mathematics, function composition is traditionally denoted with ∘ operator.
Ocaml standard library does not provide analogous operator under any name.
Batteries Included provides provides two alternatives:
_ % _
and
_ %> _
The first operator one corresponds to the classical ∘ operator routinely used in mathematics.
I.e.:
(f4 % f3 % f2 % f1) x ≜ (f4 ∘ f3 ∘ f2 ∘ f1) x
We can call it "right-to-left" composition because:
- the function we write as first (f4) will be called as last
- and the function write as last (f1) will be called as first.
The meaning of the second operator is this:
(f1 %> f2 %> f3 %> f4) x ≜ (f4 ∘ f3 ∘ f2 ∘ f1) x
We can call it "left-to-right" composition because:
- the function we write as first (f1) will be called first
- and the function we write as last (f4) will be called last
That is, the functions are written in the same order in which we write and read them.
I think that it makes sense to prefer the "left-to-right" variant because
it enables us to write functions in the same order in which they will be actually called
and it thus better fits our culture
(we read/write from left to right).
|
| | | |
| | |
| | |
| | | |
"Context.Named.{to,of}_rel_decl"
|
| | | |
| | |
| | |
| | | |
"Context.{Rel,Named}.fold_constr"
|
| | | | |
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
mainly concerning referring to "Context.{Rel,Named}.get_{id,value,type}" functions.
If multiple modules define a function with a same name, e.g.:
Context.{Rel,Named}.get_type
those calls were prefixed with a corresponding prefix
to make sure that it is obvious which function is being called.
|
| | |
| |
| |
| | |
Suggested by @ppedrot
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
| |
In some cases prior to this patch, there were two cases for the same
error function, one taking a location, the other not.
We unify them by using an option parameter, in the line with recent
changes in warnings and feedback.
This implies a bit of clean up in some places, but more importantly, is
the preparation for subsequent patches making `Loc.location` opaque,
change that could be use to improve modularity and allow a more
functional implementation strategy --- for example --- of the
beautifier.
|
| |
|
|
|
|
|
|
| |
Delimit the scope of the failure to ease potential need for debugging
the debugging printer.
Protect against one of the causes of failure (calling
get_family_sort_of with non-synchronized sigma).
|
Emilio Jesus Gallego Arias
Gaëtan Gilbert
Hugo Herbelin
Matthieu Sozeau
Pierre-Marie Pédrot
Maxime Dénès
Matthieu Sozeau
Jason Gross
Gaetan Gilbert
Matej Kosik
Matej Kosik