matita.cs.unibo.it Git - helm.git/history - helm/software/components/ng

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

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

2008-04-11	Enrico Tassi	use universe rank instead of Type0	blob \| commitdiff \| raw
2008-04-10	Claudio Sacerdoti...	The cache of objects is now used also for cofixpoints.	blob \| commitdiff \| raw \| diff to current
2008-04-10	Claudio Sacerdoti...	New: cache of translated fixpoints (to avoid the genera...	blob \| commitdiff \| raw \| diff to current
2008-04-09	Claudio Sacerdoti...	Fixed serious bug that occurred only in the following...	blob \| commitdiff \| raw \| diff to current
2008-04-09	Claudio Sacerdoti...	Grave bug fixed: Ce that point to definitions were...	blob \| commitdiff \| raw \| diff to current
2008-04-08	Claudio Sacerdoti...	Variables having a body can occur in cooked terms and...	blob \| commitdiff \| raw \| diff to current
2008-04-08	Claudio Sacerdoti...	Fix over the previous one: Var-LetIn abstractions shoul...	blob \| commitdiff \| raw \| diff to current
2008-04-08	Claudio Sacerdoti...	Cooking w.r.t. variables with bodies is now implemented...	blob \| commitdiff \| raw \| diff to current
2008-04-08	Claudio Sacerdoti...	Fix name capture in cofix.	blob \| commitdiff \| raw \| diff to current
2008-04-08	Claudio Sacerdoti...	Name capture fixed.	blob \| commitdiff \| raw \| diff to current
2008-04-08	Claudio Sacerdoti...	Seed reset before each convert_obj.	blob \| commitdiff \| raw \| diff to current
2008-04-08	Claudio Sacerdoti...	Use seed to avoid further name clashes.	blob \| commitdiff \| raw \| diff to current
2008-04-08	Claudio Sacerdoti...	Incredible, but true! Our name mangling clashed with...	blob \| commitdiff \| raw \| diff to current
2008-04-08	Claudio Sacerdoti...	Cooked objects are no longer well typed in the uncooked...	blob \| commitdiff \| raw \| diff to current
2008-04-08	Claudio Sacerdoti...	The old kernel does not accept ens whose order is diffe...	blob \| commitdiff \| raw \| diff to current
2008-04-08	Claudio Sacerdoti...	Bug fixed: the ens need not be ordered w.r.t. the decla...	blob \| commitdiff \| raw \| diff to current
2008-04-08	Claudio Sacerdoti...	fix_outty partially fixed: missing lifts in args and ens	blob \| commitdiff \| raw \| diff to current
2008-04-08	Claudio Sacerdoti...	fix_outty fixed in order to perform eta-expansion when...	blob \| commitdiff \| raw \| diff to current
2008-04-07	Claudio Sacerdoti...	Tentative (and bad!) fix of outtypes in non-dependent...	blob \| commitdiff \| raw \| diff to current
2008-04-07	Claudio Sacerdoti...	Cooking discriminated into cooking in types (using...	blob \| commitdiff \| raw \| diff to current
2008-04-07	Claudio Sacerdoti...	Cooking implemented (not tested yet).	blob \| commitdiff \| raw \| diff to current
2008-04-07	Enrico Tassi	uris relative to axioms are translated in the right way	blob \| commitdiff \| raw \| diff to current
2008-04-07	Enrico Tassi	new constants have depth = max_int insted of 0 so that...	blob \| commitdiff \| raw \| diff to current
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.

RSS Atom