]> matita.cs.unibo.it Git - helm.git/history - helm/software/components/ng_refiner/nCicRefiner.ml
eta-contraction was made on the wrong term
[helm.git] / helm / software / components / ng_refiner / nCicRefiner.ml
2009-04-06 Enrico Tassisnapshot
2009-04-01 Enrico Tassi1) mk_meta now returns also the index of the created...
2009-03-25 Enrico Tassinew tactics are almost ready
2009-03-03 Enrico Tassi- fixed hint generation, more hints are generated
2009-02-11 Enrico Tassisome work to refine objs
2008-12-19 Enrico Tassilambda case fixed, used to not properly use the expecte...
2008-12-15 Wilmer RicciottiFirst attempt to implement unification hints.
2008-12-12 Enrico Tassiadded some messages
2008-12-09 Enrico Tassiraise uncertain when a sort is not a sort but may be...
2008-12-07 Claudio Sacerdoti... Bug fixed: every time we form a Prod, we must typecheck...
2008-12-05 Claudio Sacerdoti... Debugging code removed
2008-12-05 Enrico Tassia few missing ~subst added to whd
2008-12-05 Enrico Tassicoercions are there, but not heavily tested
2008-12-04 Enrico TassiFixes:
2008-11-28 Enrico Tassiit works!
2008-11-28 Enrico Tassimetas for terms have height 3
2008-11-06 Enrico Tassibetter error messages. sorts are compared using whd
2008-10-27 Enrico Tassimany bugs fixed
2008-10-21 Enrico Tassi- mk_restricted_irl removed, the non-optimized code...
2008-10-20 Enrico Tassi...
2008-10-15 Enrico Tassisome bug fixed
2008-10-14 Enrico Tassimore work
2008-10-14 Enrico Tassiterm refinement almost done, some functions exported...
2008-10-13 Enrico Tassiinitial refiner ....
2008-09-16 Enrico Tassi...