Skip to content

Navigation Menu

Appearance settings

GitHub Copilot
Write better code with AI

GitHub Spark New
Build and deploy intelligent apps

GitHub Models New
Manage and compare prompts

GitHub Advanced Security
Find and fix vulnerabilities

Actions
Automate any workflow
Codespaces
Instant dev environments

Issues
Plan and track work

Code Review
Manage code changes

Discussions
Collaborate outside of code

Code Search
Find more, search less
Explore

Why GitHub

Documentation

GitHub Skills

Blog
Integrations

GitHub Marketplace

MCP Registry
View all features
By company size

Enterprises

Small and medium teams

Startups

Nonprofits
By use case

App Modernization

DevSecOps

DevOps

CI/CD

View all use cases
By industry

Healthcare

Financial services

Manufacturing

Government

View all industries
View all solutions
Topics

AI

DevOps

Security

Software Development

View all
Explore

Learning Pathways

Events & Webinars

Ebooks & Whitepapers

Customer Stories

Partners

Executive Insights
GitHub Sponsors
Fund open source developers
The ReadME Project
GitHub community articles
Repositories

Topics

Trending

Collections
Enterprise platform
AI-powered developer platform
Available add-ons

GitHub Advanced Security
Enterprise-grade security features

Copilot for business
Enterprise-grade AI features

Premium Support
Enterprise-grade 24/7 support
Pricing

Search code, repositories, users, issues, pull requests...

Search

Clear

Search syntax tips

Provide feedback

We read every piece of feedback, and take your input very seriously.

Include my email address so I can be contacted

Saved searches

Use saved searches to filter your results more quickly

Name

Query

To see all available qualifiers, see our documentation.

Appearance settings

You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session. You switched accounts on another tab or window. Reload to refresh your session.

Dismiss alert

LPCIC / coq-elpi Public

Notifications You must be signed in to change notification settings
Fork 67
Star 177

Code
Issues 79
Pull requests 28
Actions
Projects
Security
Insights

Additional navigation options

Code
Issues
Pull requests
Actions
Projects
Security
Insights

TC Solver: prim-proj and canonical struct#802

Draft

FissoreD wants to merge 33 commits intoLPCIC:masterLPCIC/coq-elpi:masterfrom

FissoreD:ce-compile-more-constructors1FissoreD/coq-elpi:ce-compile-more-constructors1Copy head branch name to clipboard

Conversation Commits33 (33)Checks Files changed

Draft

TC Solver: prim-proj and canonical struct#802
FissoreD wants to merge 33 commits intoLPCIC:masterfrom
FissoreD:ce-compile-more-constructors1

Commits

Commits on Apr 8, 2025

[TC] primitive constructor for fold in instance (pre-)compilation
FissoreD
committed
[TC] canonical proj solved with coq.unify-eq
FissoreD
committed
[TC] clean-term also for tc.canonical-projection
FissoreD
committed
[TC] compilation of primitive projections to their compatibility constants
FissoreD
committed
Revert "[TC] compilation of primitive projections to their compatibility constants"
FissoreD
committed
[TC] put cnonical projection in tc namespace
FissoreD
committed
remove reduntant calls to Elpi Typecheck
FissoreD
committed
[TC] local binders in evar scope during precompile + link.cs
FissoreD
committed
[TC] add TC.AddRecordFields command + better chr for canon struct
FissoreD
committed
[TC] mode ground with ground_term check + tc.link for coercions
FissoreD
committed
[TC] clean term in decompilation of goal
FissoreD
committed
[TC] add file deps in tests/importOrder/sameOrderCommand.v
FissoreD
committed
[TC] perf: fold-map fully implemented in precompile goal
FissoreD
committed
[TC] improve perf of goal compilation
FissoreD
committed
[TC] remove goal precomp and goal compile (all is done in ycompile_goal.elpi)
FissoreD
committed
[TC] refactor filenames + reorder import
FissoreD
committed
[TC] refactor of build-eta-llam-links
FissoreD
committed
[TC] avoid a backtrack
FissoreD
committed
[TC] clean compile-conclusion predicate
FissoreD
committed
[TC] link small refactor
FissoreD
committed
[TC] clean link code + unification with cs links only after a call to tc.compile.
FissoreD
committed
add _opam to .gitignore
FissoreD
committed
[TC] clearn-term on pi-decl in decompile-term-aux
FissoreD
committed
[TC] dummy clauses are local to sections
FissoreD
committed
[TC] add comment
FissoreD
committed
[TC] move time-is-active and coercion-unify in db.v
FissoreD
committed
cleanup

gares
authored and
FissoreD
committed
cleanup

gares
authored and
FissoreD
committed
cleanup

gares
authored and
FissoreD
committed
ci

gares
authored and
FissoreD
committed

Commits on Apr 9, 2025

[TC] fix
FissoreD
committed
[TC] base file loaded once
FissoreD
committed
[TC] add some doc to predicates
FissoreD
committed

Footer

© 2025 GitHub, Inc.

Footer navigation

Terms
Privacy
Security
Status
Community
Docs
Contact

You can’t perform that action at this time.