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

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

[helm.git] / helm / software / components / ng_refiner / nCicUnification.ml

2009-07-30	Claudio Sacerdoti...	Don't reinvent the wheel.	blob \| commitdiff \| raw
2009-07-24	Claudio Sacerdoti...	Beta-expansion was avoided as soon as one argument...	blob \| commitdiff \| raw \| diff to current
2009-07-20	Claudio Sacerdoti...	Debugging printf removed	blob \| commitdiff \| raw \| diff to current
2009-07-20	Claudio Sacerdoti...	Very serious bug fixed in unification, but the fix...	blob \| commitdiff \| raw \| diff to current
2009-07-20	Claudio Sacerdoti...	1) ppmetasenv and ppcontext to reduce the amount of...	blob \| commitdiff \| raw \| diff to current
2009-06-17	Claudio Sacerdoti...	Initial implementation of statuses using objects in...	blob \| commitdiff \| raw \| diff to current
2009-06-15	Enrico Tassi	huge commit regarding the grafite_status:	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-05-11	Claudio Sacerdoti...	Bug fixed: the relevance list can be shorted then leftn...	blob \| commitdiff \| raw \| diff to current
2009-04-29	Claudio Sacerdoti...	Refinement of inductive type implemented.	blob \| commitdiff \| raw \| diff to current
2009-04-06	Claudio Sacerdoti...	New tactic clear; new syntax # _; to introduce and...	blob \| commitdiff \| raw \| diff to current
2009-04-06	Enrico Tassi	tactic cases works! delift clears tags	blob \| commitdiff \| raw \| diff to current
2009-04-06	Enrico Tassi	eta-contraction was made on the wrong term	blob \| commitdiff \| raw \| diff to current
2009-04-06	Enrico Tassi	unification:	blob \| commitdiff \| raw \| diff to current
2009-04-06	Enrico Tassi	snapshot	blob \| commitdiff \| raw \| diff to current
2009-03-11	Enrico Tassi	unification hints with recursive calls do work!	blob \| commitdiff \| raw \| diff to current
2009-03-10	Enrico Tassi	unificatiom hints with premises	blob \| commitdiff \| raw \| diff to current
2009-03-10	Enrico Tassi	unification hints almost ready	blob \| commitdiff \| raw \| diff to current
2009-03-03	Enrico Tassi	- fixed hint generation, more hints are generated	blob \| commitdiff \| raw \| diff to current
2008-12-19	Enrico Tassi	added better debug_pps and add_user_provided_unificatio...	blob \| commitdiff \| raw \| diff to current
2008-12-16	Enrico Tassi	hints attached	blob \| commitdiff \| raw \| diff to current
2008-12-15	Wilmer Ricciotti	First attempt to implement unification hints.	blob \| commitdiff \| raw \| diff to current
2008-12-11	Claudio Sacerdoti...	Applications are now processed from left to right.	blob \| commitdiff \| raw \| diff to current
2008-12-05	Enrico Tassi	raise failure instead of uncertain if two terms are...	blob \| commitdiff \| raw \| diff to current
2008-11-12	Enrico Tassi	more printings	blob \| commitdiff \| raw \| diff to current
2008-11-06	Enrico Tassi	removed empty lines	blob \| commitdiff \| raw \| diff to current
2008-10-27	Enrico Tassi	many bugs fixed	blob \| commitdiff \| raw \| diff to current
2008-10-21	Enrico Tassi	- mk_restricted_irl removed, the non-optimized code...	blob \| commitdiff \| raw \| diff to current
2008-10-20	Enrico Tassi	...	blob \| commitdiff \| raw \| diff to current
2008-10-15	Enrico Tassi	subst_meta was missing	blob \| commitdiff \| raw \| diff to current
2008-10-14	Enrico Tassi	more work	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-08	Wilmer Ricciotti	Fixed a performance problem with unif_machines and...	blob \| commitdiff \| raw \| diff to current
2008-10-06	Enrico Tassi	slow example	blob \| commitdiff \| raw \| diff to current
2008-10-06	Enrico Tassi	3 nasty bugs fixed:	blob \| commitdiff \| raw \| diff to current
2008-10-03	Enrico Tassi	...	blob \| commitdiff \| raw \| diff to current
2008-10-03	Enrico Tassi	not so nice patch to small_delta_step	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	Enrico Tassi	better debuggin output	blob \| commitdiff \| raw \| diff to current
2008-10-02	Enrico Tassi	error...	blob \| commitdiff \| raw \| diff to current
2008-10-02	Enrico Tassi	another divergence case patched	blob \| commitdiff \| raw \| diff to current
2008-10-02	Enrico Tassi	to avoid a case of divergence small_delta_step checks...	blob \| commitdiff \| raw \| diff to current
2008-09-30	Enrico Tassi	unification completed	blob \| commitdiff \| raw \| diff to current
2008-09-29	Enrico Tassi	...	blob \| commitdiff \| raw \| diff to current
2008-09-25	Enrico Tassi	...	blob \| commitdiff \| raw \| diff to current
2008-09-25	Enrico Tassi	beta expand	blob \| commitdiff \| raw \| diff to current
2008-09-25	Enrico Tassi	...	blob \| commitdiff \| raw \| diff to current
2008-09-24	Enrico Tassi	...	blob \| commitdiff \| raw \| diff to current
2008-09-24	Enrico Tassi	...	blob \| commitdiff \| raw \| diff to current
2008-09-16	Enrico Tassi	...	blob \| commitdiff \| raw \| diff to current

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

RSS Atom