]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2a20f24) | patch
some fixed done in Orsay:
authorAndrea Asperti <andrea.asperti@unibo.it>
Thu, 15 Jun 2006 09:37:49 +0000 (09:37 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Thu, 15 Jun 2006 09:37:49 +0000 (09:37 +0000)
commitb09b0e4b30c429d8e050150cc4e9b94d7c205368
treeb596fed1ae552952c94fc4100f2e9bf6d5825d6ftree | snapshot
parent2a20f24b0c51947e5b3f03d31d9ffd8ce7ee5324commit | diff
some fixed done in Orsay:
- supL is called on both sides if the equation is not oriented
- contextualize_rewrites fixed if multiple equalities are used (equalities on different types)
components/tactics/paramodulation/equality.ml diff | blob | history
components/tactics/paramodulation/indexing.ml diff | blob | history
components/tactics/paramodulation/inference.ml diff | blob | history
components/tactics/paramodulation/saturation.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.