Various fixes

[helm.git] / helm / software / components / ng_paramodulation / nCicProof.ml

diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml
index 35c3c02b13b2e84202398b7fb1e7f94d3ce7b3c3..1e50999e9e14243fd6dc976f7c4eb0372c2ccaf2 100644 (file)
--- a/helm/software/components/ng_paramodulation/nCicProof.ml
+++ b/helm/software/components/ng_paramodulation/nCicProof.ml
@@ -113,7 +113,7 @@
        t vl  
     in
     let get_literal id =
-      let _, lit, vl, proof = Terms.M.find id bag in
+      let (_, lit, vl, proof),_ = Terms.M.find id bag in
       let lit =match lit with 
           | Terms.Predicate t -> assert false 
           | Terms.Equation (l,r,ty,_) ->