X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;fp=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=306104658414913ece8eef01a984f462c86bb240;hb=38c54dd8e2234836d5f3e8011c478daf7d59fa25;hp=67df0654ecf88bf3d0f73d5f7279700b9ec45a7d;hpb=8a3045a162622e8a76ffdb267309faff496ee7ec;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 67df0654e..306104658 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -194,6 +194,7 @@ module Superposition (B : Orderings.Blob) =
 
     let demodulate_once ~jump_to_right bag (id, nlit, plit, vl, pr) table =
      match nlit,plit with
+     |[literal,_], []
      |[],[literal,_] ->
       (match literal with
       | Terms.Predicate t -> assert false
@@ -259,8 +260,7 @@ module Superposition (B : Orderings.Blob) =
       | _, [], [Terms.Equation (l,r,_,_),_], vl, proof when unify ->
           (try ignore(Unif.unification (* vl *) [] l r); true
           with FoUnif.UnificationFailure _ -> false)
-      | _, [], [Terms.Equation (_,_,_,_),_], _, _ -> false
-      | _ -> assert false
+      | _ -> false
     ;;
 
     let build_new_clause bag maxvar filter rule t subst id id2 pos dir =