[TC] CS projections replaced with uvar#648

Open

FissoreD wants to merge 32 commits intoLPCIC:masterfrom FissoreD:tc-compile-more-constructors

+1,425-1,170

Commits on Oct 2, 2024

[TC] primitive constructor for fold in instance (pre-)compilation

FissoreD
authored and
gares
committed
[TC] canonical proj solved with coq.unify-eq

FissoreD
authored and
gares
committed
[TC] clean-term also for tc.canonical-projection

FissoreD
authored and
gares
committed
[TC] compilation of primitive projections to their compatibility constants

FissoreD
authored and
gares
committed
Revert "[TC] compilation of primitive projections to their compatibility constants"

FissoreD
authored and
gares
committed
[TC] put cnonical projection in tc namespace

FissoreD
authored and
gares
committed
remove reduntant calls to Elpi Typecheck

FissoreD
authored and
gares
committed
[TC] local binders in evar scope during precompile + link.cs

FissoreD
authored and
gares
committed
[TC] add TC.AddRecordFields command + better chr for canon struct

FissoreD
authored and
gares
committed
[TC] mode ground with ground_term check + tc.link for coercions

FissoreD
authored and
gares
committed
[TC] clean term in decompilation of goal

FissoreD
authored and
gares
committed
[TC] add file deps in tests/importOrder/sameOrderCommand.v

FissoreD
authored and
gares
committed
[TC] perf: fold-map fully implemented in precompile goal

FissoreD
authored and
gares
committed
[TC] improve perf of goal compilation

FissoreD
authored and
gares
committed
[TC] remove goal precomp and goal compile (all is done in ycompile_goal.elpi)

FissoreD
authored and
gares
committed
[TC] refactor filenames + reorder import

FissoreD
authored and
gares
committed
[TC] refactor of build-eta-llam-links

FissoreD
authored and
gares
committed
[TC] avoid a backtrack

FissoreD
authored and
gares
committed
[TC] clean compile-conclusion predicate

FissoreD
authored and
gares
committed
[TC] link small refactor

FissoreD
authored and
gares
committed
[TC] clean link code + unification with cs links only after a call to tc.compile.

FissoreD
authored and
gares
committed
add _opam to .gitignore

FissoreD
authored and
gares
committed
[TC] clearn-term on pi-decl in decompile-term-aux

FissoreD
authored and
gares
committed
[TC] dummy clauses are local to sections

FissoreD
authored and
gares
committed
[TC] add comment

FissoreD
authored and
gares
committed
[TC] move time-is-active and coercion-unify in db.v

FissoreD
authored and
gares
committed
cleanup
gares
committed
cleanup
gares
committed
cleanup
gares
committed
cleanup
gares
committed
ci
gares
committed
nix
gares
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[TC] CS projections replaced with uvar#648

Commits on Oct 2, 2024

[TC] primitive constructor for fold in instance (pre-)compilation

[TC] canonical proj solved with coq.unify-eq

[TC] clean-term also for tc.canonical-projection

[TC] compilation of primitive projections to their compatibility constants

Revert "[TC] compilation of primitive projections to their compatibility constants"

[TC] put cnonical projection in tc namespace

remove reduntant calls to Elpi Typecheck

[TC] local binders in evar scope during precompile + link.cs

[TC] add TC.AddRecordFields command + better chr for canon struct

[TC] mode ground with ground_term check + tc.link for coercions

[TC] clean term in decompilation of goal

[TC] add file deps in tests/importOrder/sameOrderCommand.v

[TC] perf: fold-map fully implemented in precompile goal

[TC] improve perf of goal compilation

[TC] remove goal precomp and goal compile (all is done in ycompile_goal.elpi)

[TC] refactor filenames + reorder import

[TC] refactor of build-eta-llam-links

[TC] avoid a backtrack

[TC] clean compile-conclusion predicate

[TC] link small refactor

[TC] clean link code + unification with cs links only after a call to tc.compile.

add _opam to .gitignore

[TC] clearn-term on pi-decl in decompile-term-aux

[TC] dummy clauses are local to sections

[TC] add comment

[TC] move time-is-active and coercion-unify in db.v

cleanup

cleanup

cleanup

cleanup

ci

nix