]> matita.cs.unibo.it Git - helm.git/commitdiff
Syntax error
authorAndrea Asperti <andrea.asperti@unibo.it>
Wed, 9 Dec 2009 15:53:26 +0000 (15:53 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Wed, 9 Dec 2009 15:53:26 +0000 (15:53 +0000)
helm/software/components/ng_paramodulation/superposition.ml

index fad0a12d28a7df72ad7acad75eb45abf0d70efbe..585fbe2371caf146bb2377e072cc75b37039addb 100644 (file)
@@ -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)