]> matita.cs.unibo.it Git - helm.git/commit
Some quick patch to fix elimination that used to look for
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 13 Aug 2009 17:15:16 +0000 (17:15 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 13 Aug 2009 17:15:16 +0000 (17:15 +0000)
commit5366f90df289f2ab2bd97c68643198f54ad2d2ac
tree832c8f21a9b29485de4186329a414bee201d77bb
parentd44567ba4b1a658974ee353e67c05d114c264f7f
Some quick patch to fix elimination that used to look for
nat_rect_max{CProp0,Type0}
helm/software/components/ng_tactics/nTacStatus.ml
helm/software/components/ng_tactics/nTacStatus.mli
helm/software/components/ng_tactics/nTactics.ml