matita.cs.unibo.it Git - helm.git/history - helm/software/components/ng_kernel/oCic2NCic.ml

]> matita.cs.unibo.it Git - helm.git/history - helm/software/components/ng_kernel/oCic2NCic.ml

projects / helm.git / history

summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next

[helm.git] / helm / software / components / ng_kernel / oCic2NCic.ml

2008-04-07	Enrico Tassi	new constants have depth = max_int insted of 0 so that...	blob \| commitdiff \| raw
2008-04-07	Enrico Tassi	fixed bug in translating Fix, recno was not properly...	blob \| commitdiff \| raw \| diff to current
2008-04-07	Enrico Tassi	reference type made private, added mk_constructor to...	blob \| commitdiff \| raw \| diff to current
2008-04-04	Enrico Tassi	debugging started	blob \| commitdiff \| raw \| diff to current
2008-04-02	Enrico Tassi	added translation of Set to Type0 (avoid warning)	blob \| commitdiff \| raw \| diff to current
2008-03-31	Claudio Sacerdoti...	1) Impredicative sort "Set" removed everywhere.	blob \| commitdiff \| raw \| diff to current
2008-03-25	Enrico Tassi	context for fixpoint body created in the hopefully...	blob \| commitdiff \| raw \| diff to current
2008-03-25	Enrico Tassi	ported to the Cic LetIn with explicit type	blob \| commitdiff \| raw \| diff to current
2008-02-21	Claudio Sacerdoti...	Avoid application to 0 arguments.	blob \| commitdiff \| raw \| diff to current
2008-02-20	Enrico Tassi	splat_args is now better understood and debugged: we...	blob \| commitdiff \| raw \| diff to current
2008-02-20	Enrico Tassi	added small test, fixed some bugs	blob \| commitdiff \| raw \| diff to current
2008-02-20	Enrico Tassi	many fixed in translation functions	blob \| commitdiff \| raw \| diff to current
2008-02-19	Enrico Tassi	...	blob \| commitdiff \| raw \| diff to current
2008-02-19	Enrico Tassi	snapshot inverse tranformation	blob \| commitdiff \| raw \| diff to current
2008-02-19	Enrico Tassi	transformation almost finisced, not tested	blob \| commitdiff \| raw \| diff to current
2008-02-13	Enrico Tassi	conversion half inplemented	blob \| commitdiff \| raw \| diff to current
2008-01-30	Enrico Tassi	stub functions to make all compile	blob \| commitdiff \| raw \| diff to current

Unnamed repository; edit this file 'description' to name the repository.