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

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

projects / helm.git / history

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

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

2022-12-30	Claudio Sacerdoti...	Porting to ocaml 5	blob \| commitdiff \| raw
2013-02-01	Ferruccio Guidi	- ng_refiner:	blob \| commitdiff \| raw \| diff to current
2012-07-19	Claudio Sacerdoti...	One less warning.	blob \| commitdiff \| raw \| diff to current
2012-06-29	Claudio Sacerdoti...	Bug fixed: arguments of a match are (no longer...)...	blob \| commitdiff \| raw \| diff to current
2012-01-10	Wilmer Ricciotti	Bugfix: NCicUnification.could_reduce now performs whd...	blob \| commitdiff \| raw \| diff to current
2011-06-06	Claudio Sacerdoti...	Major speed-up:	blob \| commitdiff \| raw \| diff to current
2011-06-01	Claudio Sacerdoti...	Delift used to produce not well typed substitutions...	blob \| commitdiff \| raw \| diff to current
2011-05-26	Claudio Sacerdoti...	Added "nocomposites" to coercions.	blob \| commitdiff \| raw \| diff to current
2011-01-11	Claudio Sacerdoti...	HUGE COMMIT:	blob \| commitdiff \| raw \| diff to current
2010-11-26	Andrea Asperti	- GREAT: when unifying ?1 : Type[i] with ?2: Type...	blob \| commitdiff \| raw \| diff to current
2010-11-25	Claudio Sacerdoti...	New behaviour of fo_unif: in case of ?f args == t...	blob \| commitdiff \| raw \| diff to current
2010-11-19	Andrea Asperti	Implementation of proof irrelevance finished.	blob \| commitdiff \| raw \| diff to current
2010-10-17	Enrico Tassi	backport of patches to unification	blob \| commitdiff \| raw \| diff to current
2010-09-30	Enrico Tassi	sync with stable:	blob \| commitdiff \| raw \| diff to current
2010-09-30	Claudio Sacerdoti...	Stuff moved from old Matita.	blob \| commitdiff \| raw \| diff to current

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