]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8c8ee30) | patch
Pruning generalized from Vars to applied Vars.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 15 May 2012 23:20:33 +0000 (23:20 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 15 May 2012 23:20:33 +0000 (23:20 +0000)
commitc3ef73856c5dac1d197c9d41dc61c4b2163ae354
tree35adff0d17a69c2e3672d842486bd55dfbdc3e85tree | snapshot
parent8c8ee30d3de315e954a59b3e802748099a32b54ccommit | diff
Pruning generalized from Vars to applied Vars.
Assert false since it can happen (???) that an equation
is oriented as ? M -> N   :-(
matita/components/ng_paramodulation/superposition.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.