]> matita.cs.unibo.it Git - helm.git/commitdiff
removedx a prerr_endline
authorEnrico Tassi <enrico.tassi@inria.fr>
Sat, 20 May 2006 10:07:01 +0000 (10:07 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Sat, 20 May 2006 10:07:01 +0000 (10:07 +0000)
helm/software/components/tactics/paramodulation/indexing.ml

index d69404ed4907af729bb5c3fbf53ea22ddc32b313..d35fbff34ee0f36f96236369d9b05eba7f78f5a2 100644 (file)
@@ -242,7 +242,6 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
     | [] -> None
     | candidate::tl ->
         let pos, equality = candidate in
-        prerr_endline (". " ^ Equality.string_of_equality equality);
         let (_, proof, (ty, left, right, o), metas,_) = 
           Equality.open_equality equality 
         in