]> 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)
commit2cb08b0959a375f2d542948cc0da3a4bbc551a5c
treed72ca65fd365d553a0ffa3ba5201ea5e8c423e11
parentb1ec882fae6023000ff6076e0a45f9809a6210e4
the tactic now returns as open goals the open metas in the proof
subsumption is now used correctly in given_clause_fullred
helm/software/components/tactics/paramodulation/indexing.ml
helm/software/components/tactics/paramodulation/indexing.mli
helm/software/components/tactics/paramodulation/inference.ml
helm/software/components/tactics/paramodulation/inference.mli
helm/software/components/tactics/paramodulation/saturation.ml
helm/software/components/tactics/paramodulation/saturation.mli