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

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

[helm.git] / helm / software / components / ng_tactics / nCicElim.ml

2009-10-02	Enrico Tassi	fixed bug in coercion application, input/output swapped...	blob \| commitdiff \| raw
2009-09-21	Enrico Tassi	huge commit regarding universes:	blob \| commitdiff \| raw \| diff to current
2009-09-08	Enrico Tassi	snapshot for CSC	blob \| commitdiff \| raw \| diff to current
2009-09-02	Enrico Tassi	do not fail if the inductive type is mutual, just do...	blob \| commitdiff \| raw \| diff to current
2009-07-31	Claudio Sacerdoti...	Record projections are now defined as fixpoints in...	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
2009-07-24	Claudio Sacerdoti...	Function to map NCic.term to CicNotationPt.term finished.	blob \| commitdiff \| raw \| diff to current
2009-07-21	Claudio Sacerdoti...	Debugging code removed.	blob \| commitdiff \| raw \| diff to current
2009-07-21	Claudio Sacerdoti...	Record projections are now automatically generated...	blob \| commitdiff \| raw \| diff to current
2009-07-20	Claudio Sacerdoti...	1) The NG kernel now accepts only usage of declared...	blob \| commitdiff \| raw \| diff to current
2009-07-17	Claudio Sacerdoti...	More info to refine empty types elimination.	blob \| commitdiff \| raw \| diff to current
2009-07-17	Claudio Sacerdoti...	Debugging code commented out.	blob \| commitdiff \| raw \| diff to current
2009-07-17	Claudio Sacerdoti...	Bug fixed: singleton application.	blob \| commitdiff \| raw \| diff to current
2009-07-17	Claudio Sacerdoti...	New suffixes for elimination principles:	blob \| commitdiff \| raw \| diff to current
2009-07-17	Claudio Sacerdoti...	Generation of inductive principle for Type[0].	blob \| commitdiff \| raw \| diff to current
2009-07-15	Enrico Tassi	ncopy partially implemented and fixed (a ?) chain to...	blob \| commitdiff \| raw \| diff to current
2009-06-03	Claudio Sacerdoti...	Huge commit with several changes:	blob \| commitdiff \| raw \| diff to current
2009-05-15	Claudio Sacerdoti...	Cosmetic.	blob \| commitdiff \| raw \| diff to current
2009-05-12	Claudio Sacerdoti...	All weakly positive types but imbricated ones are now...	blob \| commitdiff \| raw \| diff to current
2009-05-11	Claudio Sacerdoti...	- non_punctuational_tacticals ported to NG	blob \| commitdiff \| raw \| diff to current

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

RSS Atom