]> matita.cs.unibo.it Git - helm.git/history - components/tactics/paramodulation/equality_retrieval.ml
Bugs fixed in merging of composite coercions. In particular the imperative
[helm.git] / components / tactics / paramodulation / equality_retrieval.ml
2006-10-03 Enrico Tassicommented out are_convertible in is_identity
2006-10-03 Andrea AspertiChanged auto from implicit to option and renamed a...
2006-09-29 Enrico Tassinew version of auto that is able to prove the irrationa...