]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9d82955) | patch
New management of the resulting substitution in deep eq.
authorAndrea Asperti <andrea.asperti@unibo.it>
Fri, 28 Oct 2011 08:40:50 +0000 (08:40 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Fri, 28 Oct 2011 08:40:50 +0000 (08:40 +0000)
commitb78de5584633b864248519d9f7cd9f86a0005c24
tree17622cd437aa897b265c7679e3f24b3067ceb420tree | snapshot
parent9d829553caad3b96314180a8dcd0b82e5c39b243commit | diff
New management of the resulting substitution in deep eq.
We reduced several time the goal vs the active table, possibly
resulting in a clash of names generating cyclic substitutions.
matita/components/ng_paramodulation/nCicProof.ml diff | blob | history
matita/components/ng_paramodulation/superposition.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.