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-10-22	Enrico Tassi	new instantiate, only known bug is w.r.t. in/out scope...	blob \| commitdiff \| raw
2009-10-16	Enrico Tassi	new lambda instros and better logging	blob \| commitdiff \| raw \| diff to current
2009-10-15	Claudio Sacerdoti...	Profiling code integrated.	blob \| commitdiff \| raw \| diff to current
2009-10-14	Enrico Tassi	hints were not used by reduction machines on heads	blob \| commitdiff \| raw \| diff to current
2009-10-12	Claudio Sacerdoti...	1) Bug fixed: the case Meta(i) vs Meta(i) was handled...	blob \| commitdiff \| raw \| diff to current
2009-10-06	Enrico Tassi	unification pps can be activated by the menu debug	blob \| commitdiff \| raw \| diff to current
2009-10-02	Enrico Tassi	hints input is cleared from projection redexes	blob \| commitdiff \| raw \| diff to current
2009-10-01	Enrico Tassi	- delift_type_wrt_term fixed in many ways	blob \| commitdiff \| raw \| diff to current
2009-10-01	Enrico Tassi	instantiate merges tags	blob \| commitdiff \| raw \| diff to current
2009-10-01	Enrico Tassi	added sortification for (? args), untested code	blob \| commitdiff \| raw \| diff to current
2009-10-01	Enrico Tassi	sortification simplified	blob \| commitdiff \| raw \| diff to current
2009-09-30	Enrico Tassi	rewritten instantiate code	blob \| commitdiff \| raw \| diff to current
2009-09-30	Claudio Sacerdoti...	New datatype for metasenv/subst: full fledged attribute...	blob \| commitdiff \| raw \| diff to current
2009-09-30	Claudio Sacerdoti...	Better (but still broken) fix for the case ?sort vs...	blob \| commitdiff \| raw \| diff to current
2009-09-29	Claudio Sacerdoti...	1) improved (???) debugging, with	blob \| commitdiff \| raw \| diff to current
2009-09-29	Claudio Sacerdoti...	The unification does not longer use the refiner (urrah!)	blob \| commitdiff \| raw \| diff to current
2009-09-28	Enrico Tassi	better debug pp	blob \| commitdiff \| raw \| diff to current
2009-09-21	Enrico Tassi	new implementation of delift_type_wrt_term, that call...	blob \| commitdiff \| raw \| diff to current
2009-09-21	Enrico Tassi	huge commit regarding universes:	blob \| commitdiff \| raw \| diff to current
2009-09-15	Enrico Tassi	improved check in delift for flexible lc entries.	blob \| commitdiff \| raw \| diff to current
2009-09-10	Enrico Tassi	to me, the problem:	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-08-14	Claudio Sacerdoti...	Since the introduction of saturation, an assert false...	blob \| commitdiff \| raw \| diff to current
2009-08-13	Claudio Sacerdoti...	fix_sorts (cfr. previous commit) used to break too...	blob \| commitdiff \| raw \| diff to current
2009-08-13	Claudio Sacerdoti...	Let's refresh the universe to avoid assert failure.	blob \| commitdiff \| raw \| diff to current
2009-07-30	Claudio Sacerdoti...	Don't reinvent the wheel.	blob \| commitdiff \| raw \| diff to current
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