C

Coq ELPI

Settings | Report Duplicate

1

I Use This!

High Activity

Commits : Listings

Analyzed about 21 hours ago. based on code collected about 21 hours ago.

Commit Message	Contributor	Files Modified	Lines Added	Lines Removed	Code Location	Date
Jul 29, 2024 — Jul 29, 2025 Showing page 103 of 122 Search / Filter on:
param1: export reali and realiR to the clients	Enrico Tassi	More...				about 7 years ago
derive.invert	Enrico Tassi	More...				about 7 years ago
coq-lib: coq.typecheck-ind-decl	Enrico Tassi	More...				about 7 years ago
HOAS: support for non-uniform parameters in indt-decl	Enrico Tassi	More...				about 7 years ago
fix injection	Enrico Tassi	More...				about 7 years ago
derive.eq: qualify Require	Enrico Tassi	More...				about 7 years ago
derive.bcongr	Enrico Tassi	More...				about 7 years ago
update coq	Enrico Tassi	More...				about 7 years ago
eqOK: comment out incomplete code	Enrico Tassi	More...				about 7 years ago
remove elpi submodule (now an opam package)	Enrico Tassi	More...				about 7 years ago
Merge commit 'b1f6b7ff66e6032a3c3faf915d5b79746159cf24' into coq-master	Enrico Tassi	More...				about 7 years ago
param1P: fix (works for inductives using a container)	Enrico Tassi	More...				about 7 years ago
wip	Enrico Tassi	More...				about 7 years ago
silence error when elpi is not in PATH	Enrico Tassi	More...				about 7 years ago
silence error when elpi is not in PATH	Enrico Tassi	More...				about 7 years ago
Update elpi	Enrico Tassi	More...				about 7 years ago
Update elpi	Enrico Tassi	More...				about 7 years ago
HOAS: switch to EConstr.t	Enrico Tassi	More...				about 7 years ago
.merlin: make it work when elpi is installed via findlib	Enrico Tassi	More...				about 7 years ago
some progress on eqOK	Enrico Tassi	More...				about 7 years ago
travis: be verbose	Enrico Tassi	More...				about 7 years ago
induction: works for W	Enrico Tassi	More...				about 7 years ago
param1P: db entry for UnitPred and ArrowPred	Enrico Tassi	More...				about 7 years ago
param1: provide a db entry for the Arrow	Enrico Tassi	More...				about 7 years ago
test for constrsimplifier	Enrico Tassi	More...				about 7 years ago
Elpi Db ".." now lets one accumulate in a Db	Enrico Tassi	More...				about 7 years ago
remove spy	Enrico Tassi	More...				about 7 years ago
derive: add induction + constsimplifier	Enrico Tassi	More...				about 7 years ago
derive.*.main: the input is a term, not a string	Enrico Tassi	More...				about 7 years ago
derive.induction: fully schematic (to be simplified later)	Enrico Tassi	More...				about 7 years ago

←
1
2
…
99
100
101
102
103
104
105
106
107
…
121
122
→