]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d2ad19f) | 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)
commit3df775cea96aae2d25dd9b47f9491711abc1c8fb
tree6f25cb54d624410864285e80d0b38d1bfd9ab04ftree | snapshot
parentd2ad19f46b30ed0f873635289d89bfe46e04ffb6commit | 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)
helm/software/components/tactics/paramodulation/equality.ml diff | blob | history
helm/software/components/tactics/paramodulation/indexing.ml diff | blob | history
helm/software/components/tactics/paramodulation/inference.ml diff | blob | history
helm/software/components/tactics/paramodulation/saturation.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.