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

2009-10-16	Enrico Tassi	removed optimization potentially unsound	blob \| commitdiff \| raw
2009-10-08	Claudio Sacerdoti...	A new switch to activate/deactive nCicReduction pretty...	blob \| commitdiff \| raw \| diff to current
2009-10-07	Claudio Sacerdoti...	Performance improvement by preserving more sharing...	blob \| commitdiff \| raw \| diff to current
2009-10-02	Enrico Tassi	projections redex (proj (mk_foo ...)) where mk_foo	blob \| commitdiff \| raw \| diff to current
2009-09-21	Enrico Tassi	huge commit regarding universes:	blob \| commitdiff \| raw \| diff to current
2009-09-04	Enrico Tassi	Reduction speedup (a.k.a. better sharing):	blob \| commitdiff \| raw \| diff to current
2009-05-17	Claudio Sacerdoti...	alpha_eq defined and exported	blob \| commitdiff \| raw \| diff to current
2009-05-15	Claudio Sacerdoti...	Patch to add a debugging string to HExtlib.split_nth...	blob \| commitdiff \| raw \| diff to current
2009-05-14	Ferruccio Guidi	- hExtlib: added debugging information for split_nth	blob \| commitdiff \| raw \| diff to current
2009-04-29	Claudio Sacerdoti...	Refinement of inductive type implemented.	blob \| commitdiff \| raw \| diff to current
2009-04-01	Enrico Tassi	added tentative elim	blob \| commitdiff \| raw \| diff to current
2009-03-03	Enrico Tassi	- fixed hint generation, more hints are generated	blob \| commitdiff \| raw \| diff to current
2009-01-30	Enrico Tassi	fix convertibility in case of application test_eq_only...	blob \| commitdiff \| raw \| diff to current
2008-12-16	Enrico Tassi	previous change was causing divergence	blob \| commitdiff \| raw \| diff to current
2008-12-16	Enrico Tassi	fixed a bug, it used to report o wrong is_normal bit...	blob \| commitdiff \| raw \| diff to current
2008-12-05	Enrico Tassi	a few missing ~subst added to whd	blob \| commitdiff \| raw \| diff to current
2008-10-27	Enrico Tassi	metasenv passed to get_relevance, Metas that stand...	blob \| commitdiff \| raw \| diff to current
2008-10-13	Enrico Tassi	better error message	blob \| commitdiff \| raw \| diff to current
2008-10-13	Enrico Tassi	NCicReduction.reduce_machine returns a boolean stating...	blob \| commitdiff \| raw \| diff to current
2008-10-03	Enrico Tassi	- NCicPp.ppterm applies the substitution	blob \| commitdiff \| raw \| diff to current
2008-10-03	Wilmer Ricciotti	Final implementation of proof irrelevant conversion...	blob \| commitdiff \| raw \| diff to current
2008-09-30	Enrico Tassi	unification completed	blob \| commitdiff \| raw \| diff to current
2008-09-24	Enrico Tassi	...	blob \| commitdiff \| raw \| diff to current
2008-08-21	Claudio Sacerdoti...	Avoid warning.	blob \| commitdiff \| raw \| diff to current
2008-06-13	Wilmer Ricciotti	final relevance check	blob \| commitdiff \| raw \| diff to current
2008-06-10	Wilmer Ricciotti	relevance check for Match	blob \| commitdiff \| raw \| diff to current
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