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/nCic.ml

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

2009-10-22	Enrico Tassi	new instantiate, only known bug is w.r.t. in/out scope...	blob \| commitdiff \| raw
2009-09-30	Claudio Sacerdoti...	New datatype for metasenv/subst: full fledged attribute...	blob \| commitdiff \| raw \| diff to current
2009-09-30	Wilmer Ricciotti	Added initial support for inversion principles in Matit...	blob \| commitdiff \| raw \| diff to current
2009-09-27	Enrico Tassi	fixpoint have attributes for pragma (i.e. they can...	blob \| commitdiff \| raw \| diff to current
2009-09-21	Enrico Tassi	huge commit regarding universes:	blob \| commitdiff \| raw \| diff to current
2009-07-28	Claudio Sacerdoti...	Introduction of vectors of implicit (only for NG).	blob \| commitdiff \| raw \| diff to current
2008-10-13	Enrico Tassi	initial refiner ....	blob \| commitdiff \| raw \| diff to current
2008-09-19	Enrico Tassi	more comments and compare function for URI exported	blob \| commitdiff \| raw \| diff to current
2008-08-12	Wilmer Ricciotti	Fixed two legacy comments	blob \| commitdiff \| raw \| diff to current
2008-05-19	Claudio Sacerdoti...	CProp dropped in favour of a cprop universe exported...	blob \| commitdiff \| raw \| diff to current
2008-05-16	Enrico Tassi	added new implementation of universes	blob \| commitdiff \| raw \| diff to current
2008-05-14	Claudio Sacerdoti...	New licence used uniformly everywhere.	blob \| commitdiff \| raw \| diff to current
2008-05-13	Claudio Sacerdoti...	Type of conjecture and subst_entry made uniform.	blob \| commitdiff \| raw \| diff to current
2008-04-15	Enrico Tassi	added comment	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-27	Enrico Tassi	removed FSF header	blob \| commitdiff \| raw \| diff to current
2008-02-19	Enrico Tassi	transformation almost finisced, not tested	blob \| commitdiff \| raw \| diff to current
2008-02-18	Enrico Tassi	some bits of reduction, reusing psubst	blob \| commitdiff \| raw \| diff to current
2008-02-13	Enrico Tassi	conversion half inplemented	blob \| commitdiff \| raw \| diff to current
2008-02-13	Enrico Tassi	substituion and lifting implemented	blob \| commitdiff \| raw \| diff to current
2008-02-13	Enrico Tassi	factorized common components of objects	blob \| commitdiff \| raw \| diff to current
2008-02-13	Enrico Tassi	added Local pragma, moved leftno and inductive into...	blob \| commitdiff \| raw \| diff to current
2008-02-13	Enrico Tassi	added leftno to indtypes, better indentation and comments	blob \| commitdiff \| raw \| diff to current
2008-02-12	Enrico Tassi	nCic almost finished	blob \| commitdiff \| raw \| diff to current
2008-02-05	Enrico Tassi	cic defined (half)	blob \| commitdiff \| raw \| diff to current
2008-02-05	Enrico Tassi	reindent	blob \| commitdiff \| raw \| diff to current
2008-02-05	Enrico Tassi	uri -> reference	blob \| commitdiff \| raw \| diff to current
2008-01-30	Enrico Tassi	stub functions to make all compile	blob \| commitdiff \| raw \| diff to current
2008-01-30	Enrico Tassi	basic organization of the new kernel	blob \| commitdiff \| raw \| diff to current

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

RSS Atom