FissoreD coq-elpi issues - Githubissues

FissoreD / coq-elpi

Coq plugin embedding elpi

GNU Lesser General Public License v2.1

0 stars 0 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Solving premises with an already existing _solution_

#20 FissoreD opened 4 days ago
3
Compilation of projections is not clever ?

#19 FissoreD opened 5 days ago
1
Subgoals are put into the shelf

#18 FissoreD closed 5 days ago
0
Sealed goal for mode should be resumed if progress

#17 FissoreD opened 2 weeks ago
2
Typeclasses eauto does not call elpi's solver

#16 FissoreD opened 2 weeks ago
0
Coq elpi eta contr rebase

#15 FissoreD closed 2 weeks ago
0
Benchmark

#14 FissoreD opened 2 weeks ago
0
Always eta-contract solution

#13 FissoreD opened 2 weeks ago
0
Mode + Link activation (Loop even if force beta-link)

#12 FissoreD opened 3 weeks ago
0
Mode + Link activation (HO variable)

#11 FissoreD opened 3 weeks ago
0
No constraint on evar with type class

#10 FissoreD opened 3 weeks ago
0
Partial evaluation

#9 FissoreD opened 1 month ago
0
Create mapping coq evars -> elpi evar (to avoid typechecking while solving)

#8 FissoreD closed 1 month ago
0
This should pass: maybe-beta approx seems wrong

#7 FissoreD closed 1 month ago
1
Force links when input of a subsequent premise

#6 FissoreD closed 3 weeks ago
1
Typeclasses eauto

#5 FissoreD opened 1 month ago
1
Occur check

#4 FissoreD opened 1 month ago
0
Scope check is too expensive

#3 FissoreD opened 1 month ago
0
Link activation

#2 FissoreD opened 2 months ago
0
Compiler HO-unif-for free

#1 FissoreD closed 1 month ago
0