matita.cs.unibo.it Git - helm.git/commit

]> matita.cs.unibo.it Git - helm.git/commit

projects / helm.git / commit

summary | shortlog | log | commit | commitdiff | tree
(parent: 91f0c0e) | patch

author	Enrico Tassi <enrico.tassi@inria.fr>
	Wed, 6 May 2009 14:26:06 +0000 (14:26 +0000)
committer	Enrico Tassi <enrico.tassi@inria.fr>
	Wed, 6 May 2009 14:26:06 +0000 (14:26 +0000)
commit	25564c06c570e5ab9be455904c0b381842f8d4c4
tree	b5d1633d8e397b1cb3ee8b823f1f29ab7b026e86	tree \| snapshot
parent	91f0c0e84bfe6bf22e960d466e16f7260a2882ee	commit \| diff

apply and auto.equational_case call saturation.solve_narrowing
that performs goal inference and demodulation

14 files changed:

helm/software/components/tactics/auto.ml		diff \| blob \| history
helm/software/components/tactics/automationCache.ml		diff \| blob \| history
helm/software/components/tactics/declarative.ml		diff \| blob \| history
helm/software/components/tactics/paramodulation/equality.ml		diff \| blob \| history
helm/software/components/tactics/paramodulation/equality.mli		diff \| blob \| history
helm/software/components/tactics/paramodulation/indexing.ml		diff \| blob \| history
helm/software/components/tactics/paramodulation/indexing.mli		diff \| blob \| history
helm/software/components/tactics/paramodulation/saturation.ml		diff \| blob \| history
helm/software/components/tactics/paramodulation/saturation.mli		diff \| blob \| history
helm/software/matita/library/Q/nat_fact/times.ma		diff \| blob \| history
helm/software/matita/library/R/r.ma		diff \| blob \| history
helm/software/matita/library/didactic/exercises/duality.ma		diff \| blob \| history
helm/software/matita/library/nat/gcd.ma		diff \| blob \| history
helm/software/matita/library/nat/ord.ma		diff \| blob \| history

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