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

2008-05-15	Enrico Tassi	height of constants properly handled	blob \| commitdiff \| raw
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.