From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 9 Dec 2009 15:53:26 +0000 (+0000)
Subject: Syntax error
X-Git-Tag: make_still_working~3177
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=846c22b353bed991d0504818fa58e5ed65dec670;p=helm.git

Syntax error
---

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index fad0a12d2..585fbe237 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -627,7 +627,7 @@ module Superposition (B : Orderings.Blob) =
          | None -> Some (bag,clause)
          | Some (bag,maxvar,cl,subst) -> 
              debug (lazy "Goal subsumed");
-             raise (Success (bag,maxvar,cl)))
+             raise (Success (bag,maxvar,cl))
 (*
         match is_subsumed ~unify:true bag maxvar clause table with
         | None -> Some (bag, clause)