]> matita.cs.unibo.it Git - helm.git/history - helm/software/components/ng_refiner/nCicCoercion.ml
match_coercion gives back the saturations, not the arity:
[helm.git] / helm / software / components / ng_refiner / nCicCoercion.ml
2009-07-15 Enrico Tassimatch_coercion gives back the saturations, not the...
2009-07-13 Claudio Sacerdoti... Coercion hiding implemented. Notes:
2009-07-10 Enrico Tassiinitial implementation of coercion composition
2009-07-09 Enrico Tassiinitial implementation of `ncoercion name : type :...
2009-06-19 Claudio Sacerdoti... Good:
2009-06-18 Claudio Sacerdoti... Objects are now used to represent also the tactic status.
2009-06-17 Claudio Sacerdoti... Initial implementation of statuses using objects in...
2009-06-15 Enrico Tassihuge commit regarding the grafite_status:
2008-12-12 Enrico Tassiadded empty_db, usefull to avoid translating all old...
2008-12-09 Enrico Tassibetter coercions indexing and lookup
2008-12-05 Claudio Sacerdoti... Debugging instructions removed.
2008-12-05 Enrico Tassia few missing ~subst added to whd
2008-12-05 Enrico Tassicoercions are there, but not heavily tested