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

2008-05-19	Claudio Sacerdoti...	CProp dropped in favour of a cprop universe exported...	blob \| commitdiff \| raw
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