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

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

2008-06-10	Wilmer Ricciotti	relevance check for Match	blob \| commitdiff \| raw
2008-06-09	Wilmer Ricciotti	more proof irrelevance	blob \| commitdiff \| raw \| diff to current
2008-06-04	Wilmer Ricciotti	Proof-irrelevance check for all applications (first...	blob \| commitdiff \| raw \| diff to current
2008-05-30	Enrico Tassi	thanks to the fact that we convert well typed term...	blob \| commitdiff \| raw \| diff to current
2008-05-29	Enrico Tassi	unused variables removed	blob \| commitdiff \| raw \| diff to current
2008-05-19	Enrico Tassi	added leftno to references f inductive types and constr...	blob \| commitdiff \| raw \| diff to current
2008-05-18	Claudio Sacerdoti...	Synch with the paper.	blob \| commitdiff \| raw \| diff to current
2008-05-16	Enrico Tassi	added new implementation of universes	blob \| commitdiff \| raw \| diff to current
2008-05-16	Enrico Tassi	meta VS meta in alpha_eq honors substitution	blob \| commitdiff \| raw \| diff to current
2008-05-16	Enrico Tassi	types where compared without lookig at test_eq_only	blob \| commitdiff \| raw \| diff to current
2008-05-15	Enrico Tassi	First implementation of irrelevance in conversion.	blob \| commitdiff \| raw \| diff to current
2008-05-15	Enrico Tassi	Typo fixed.	blob \| commitdiff \| raw \| diff to current
2008-05-15	Enrico Tassi	Major code semplification and bugs removed (thanks...	blob \| commitdiff \| raw \| diff to current
2008-05-15	Andrea Asperti	Removed two args from psubst.	blob \| commitdiff \| raw \| diff to current
2008-05-15	Enrico Tassi	height of constants properly handled	blob \| commitdiff \| raw \| diff to current
2008-05-14	Enrico Tassi	partial implementation of reduction up to a given height	blob \| commitdiff \| raw \| diff to current
2008-05-13	Enrico Tassi	wrong test equality only fixed	blob \| commitdiff \| raw \| diff to current
2008-05-13	Enrico Tassi	convertibility was taking a metasenv but not using it	blob \| commitdiff \| raw \| diff to current
2008-05-12	Enrico Tassi	height is stored in the reference, no need to fetch...	blob \| commitdiff \| raw \| diff to current
2008-05-05	Enrico Tassi	get_check_fix and cofix unified, bug regarding debruijn...	blob \| commitdiff \| raw \| diff to current
2008-05-05	Enrico Tassi	removed dead code	blob \| commitdiff \| raw \| diff to current
2008-04-30	Claudio Sacerdoti...	Reducing an open term should not be an error (or should...	blob \| commitdiff \| raw \| diff to current
2008-04-15	Enrico Tassi	get_checked_fix -> get_checked_fixes	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-03-25	Enrico Tassi	new are_convertible and head_beta_reduce	blob \| commitdiff \| raw \| diff to current
2008-02-19	Enrico Tassi	initial steps of convertibility	blob \| commitdiff \| raw \| diff to current
2008-02-18	Enrico Tassi	some bits of reduction, reusing psubst	blob \| commitdiff \| raw \| diff to current

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

RSS Atom