]> matita.cs.unibo.it Git - helm.git/commit
1) added simplification of actives w.r.t. selected
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 10 Jun 2009 16:43:48 +0000 (16:43 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 10 Jun 2009 16:43:48 +0000 (16:43 +0000)
commit96c91e470f670018df67c9cbff62fa06e3b57c5e
treef90d4ac3709c8dac1fcb21cbe4b4efb997185821
parenta99b3bf44964a6a3d56d752efbdc2c962ce24d08
1) added simplification of actives w.r.t. selected
2) added simple main loop (look at the comment for a possible optimization)
helm/software/components/ng_paramodulation/paramod.ml
helm/software/components/ng_paramodulation/pp.ml
helm/software/components/ng_paramodulation/superposition.ml
helm/software/components/ng_paramodulation/superposition.mli
helm/software/components/ng_paramodulation/terms.ml
helm/software/components/ng_paramodulation/terms.mli
helm/software/matita/tests/paratest.ma