[TC] CS projections replaced with uvar - #648
Conversation
|
Note that the compilation with uvar for projections in this PR only addresses instances compilation |
|
I'm a bit lost, the test passes but I don't see how the new term constructor is compiled... miracle? 😀 |
|
The precompilator transforms a term like Here I decompile tc.canonical-projection (during the elpi's rule creation): I replace the sub-term with a fresh elpi-var Am I clarifying your remark ? |
3eceb49 to
78c7545
Compare
b1c455e to
ad0b8dc
Compare
dc047a6 to
f348d07
Compare
a015aeb to
7a07b58
Compare
e140d15 to
25de1d1
Compare
…ity constants" This reverts commit 6c63978.
This aims to solve the compilation error produced by the compilation of
```
Module foo.
Class B (i : nat).
Section s.
(* Class with coercion depending on section parameters *)
Context (A : Type).
Class C (i : A) : Set := {
x (x : A) :: B 3
}.
End s.
End foo.
```
a9d89b5 to
7986110
Compare
|
@CohenCyril this job https://github.com/LPCIC/coq-elpi/actions/runs/11143050022/job/30967371306?pr=648 |
|
I think this can be closed in favour of #1045 |
2 participants
If a subterm is a (primitive) projection, it is replaced with fresh elpi variable
This variable and the original subterm are related by the coq.unify-eq predicate, to ensure
that each subterm of a class call correctly unifies with the corresponding subterm in the instance.
Here the test for this PR