]> matita.cs.unibo.it Git - helm.git/commit
the tactic now returns as open goals the open metas in the proof
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 5 Apr 2006 12:07:51 +0000 (12:07 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 5 Apr 2006 12:07:51 +0000 (12:07 +0000)
commitbc532ce9c59e1644e02e6c0663855164c2400a40
tree41fc500cec4215234e9b78d710f2b99ca526264e
parent21933bca0834a45119f567b17b6f641113b881bb
the tactic now returns as open goals the open metas in the proof
subsumption is now used correctly in given_clause_fullred
components/tactics/paramodulation/indexing.ml
components/tactics/paramodulation/indexing.mli
components/tactics/paramodulation/inference.ml
components/tactics/paramodulation/inference.mli
components/tactics/paramodulation/saturation.ml
components/tactics/paramodulation/saturation.mli