| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
This works for contexts in Definition and co, but not yet for "fun" and co.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The motivations are:
- To reflect the concrete syntax more closely.
- To factorize the different places where "contexts" are internalized:
before this patch, there is a different treatment of `Definition f
'(x,y) := x+y` and `Definition f := fun '(x,y) => x+y`, and a hack
to interpret `Definition f `pat := c : t`. With the patch, the fix
to avoid seeing a variable named `pat` works for both `fun 'x =>
...` and `Definition f 'x := ...`.
The drawbacks are:
- Counterpart to reflecting the concrete syntax more closerly, there
are more redundancies in the syntax. For instance, the case `CLetIn
(na,b,t,c)` can appears also in the form `CProdN (CLocalDef
(na,b,t)::rest,d)` and `CLambdaN (CLocalDef (na,b,t)::rest,d)`.
- Changes in the API, hence adaptation of plugins referring to `constr_expr` needed.
|
| | |
|
| |
|
|
| |
Was apparently forgotten in a67bd7f9.
|
| |\
| |
| |
| | |
constraints.
|
| | |
| |
| |
| |
| | |
No using a mutable counter to skip them, instead we keep them in the
environment.
|
| |/
|
|
|
| |
There was no test in the test-suite checking for double with-def constraints
in module typing.
|
| |\ |
|
| | | |
|
| | | |
|
| | | |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This fixes #6350 (and even comes with a test case).
Refering to other directories as `-R … ""` is maybe not best practice,
but some people out there do it, so as long as it does not cause too
much trouble, we can continue to support it.
|
| |\ \ \ |
|
| |\ \ \ \
| |_|/ /
|/| | | |
|
| | | |/ |
|
| |\ \ \ |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
information.
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \
| |_|_|_|_|/
|/| | | | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This ensures by construction that we never infer constraints outside
the variance model.
|
| | |_|/ / /
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Since cumulativity of an inductive type is the universe constraints
which make a term convertible with its universe-renamed copy, the only
constraints we can get are between a universe and its copy.
As such we do not need to be able to represent arbitrary constraints
between universes and copied universes in a double-sized ucontext,
instead we can just keep around an array describing whether a bound
universe is covariant, invariant or irrelevant (CIC has no
contravariant conversion rule).
Printing is fairly obtuse and should be improved: when we print the
CumulativityInfo we add marks to the universes of the instance: = for
invariant, + for covariant and * for irrelevant. ie
Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }.
Print Foo.
gives
Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo
{ foo : Type@{i} -> Type@{j} }
(* =i +j *k |= *)
|
| | |/ / /
|/| | | |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| | |_|/ / /
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
There is no way today to distinguish primitive projections from
compatibility constants, at least in the case of a record without
parameters.
We remedy to this by always using the r.(p) syntax when printing
primitive projections, even with Set Printing All.
The input syntax r.(p) is still elaborated to GApp, so that we can preserve
the compatibility layer. Hopefully we can make up a plan to get rid of that
layer, but it will require fixing a few problems.
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | | |
Fixes BZ#5726.
|
| | |/ / /
|/| | | |
|
| |\ \ \ \
| |_|/ /
|/| | |
| | | | |
for primitive projections
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| | |_|/ / /
|/| | | | |
|
| | | | | | |
|
| |\ \ \ \ \
| |/ / / /
|/| | | | |
|
| |\ \ \ \ \ |
|
| | | | | | | |
|
| | | | | | | |
|
| | | |/ / /
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Fixes #6490.
`prod_applist_assum` is copied from `kernel/term.ml` to `engine/termops.ml`,
and adjusted to work with econstr.
This change uncovered a bug in `Hipattern.match_with_nodep_ind`, where
`has_nodep_prod_after` counts both products and let-ins, but was only
being passed `mib.mind_nparams`, which does not count let-ins.
Replaced with (Context.Rel.length mib.mind_params_ctxt).
|
| |\ \ \ \ \
| |_|/ / /
|/| | | | |
|
| | | | | | |
|
| | | | | | |
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \ |
|
| | | | | | | | |
|
| | |/ / / / /
|/| | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
PRINT_LOGS can be used for interactive calls, eg
make report PRINT_LOGS=1
|
| |\ \ \ \ \ \ |
|
| | |/ / / / /
|/| | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
The main contender was the abstract tactic that was generating useless
constraints for polymorphic subproofs that happened to contain themselves
monomorphic subproofs. We had to fix the test-suite for one particular
corner-case instance that looked more like a bug than anything else.
|
| | | | | | | |
|
| | | | | | | |
|
Hugo Herbelin
Maxime Dénès
Gaëtan Gilbert
Pierre-Marie Pédrot
Ralf Jung
Joachim Breitner
Paul Steckler
Tej Chajed
Cyprien Mangin
Jasper Hugunin
Théo Zimmermann