]> matita.cs.unibo.it Git - helm.git/history - matita/components/ng_refiner/nCicUnification.ml
Proved old axiom.
[helm.git] / matita / components / ng_refiner / nCicUnification.ml
2012-07-19 Claudio Sacerdoti... One less warning.
2012-06-29 Claudio Sacerdoti... Bug fixed: arguments of a match are (no longer...)...
2012-01-10 Wilmer RicciottiBugfix: NCicUnification.could_reduce now performs whd...
2011-06-06 Claudio Sacerdoti... Major speed-up:
2011-06-01 Claudio Sacerdoti... Delift used to produce not well typed substitutions...
2011-05-26 Claudio Sacerdoti... Added "nocomposites" to coercions.
2011-01-11 Claudio Sacerdoti... HUGE COMMIT:
2010-11-26 Andrea Asperti- GREAT: when unifying ?1 : Type[i] with ?2: Type...
2010-11-25 Claudio Sacerdoti... New behaviour of fo_unif: in case of ?f args == t...
2010-11-19 Andrea AspertiImplementation of proof irrelevance finished.
2010-10-17 Enrico Tassibackport of patches to unification
2010-09-30 Enrico Tassisync with stable:
2010-09-30 Claudio Sacerdoti... Stuff moved from old Matita.