matita.cs.unibo.it Git - helm.git/history - helm/software/components/ng_refiner/nCicUnification.mli

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

projects / helm.git / history

summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next

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

2009-10-22	Enrico Tassi	new instantiate, only known bug is w.r.t. in/out scope...	blob \| commitdiff \| raw
2009-10-06	Enrico Tassi	unification pps can be activated by the menu debug	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-09-29	Claudio Sacerdoti...	The unification does not longer use the refiner (urrah!)	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-08-13	Claudio Sacerdoti...	fix_sorts (cfr. previous commit) used to break too...	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-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-04-29	Claudio Sacerdoti...	Refinement of inductive type implemented.	blob \| commitdiff \| raw \| diff to current
2008-12-15	Wilmer Ricciotti	First attempt to implement unification hints.	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.