]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/content2pres.ml
Debugging infos removed.
[helm.git] / helm / ocaml / cic_transformations / content2pres.ml
index e8699b8b4445d24f04d585b6c7c21dbbcbb18ada..a57ec0396731758266625b10a726370e820b6197 100644 (file)
@@ -304,9 +304,6 @@ and proof2pres term2pres p =
             | None -> 
                 prerr_endline "NO NAME!!"; assert false) 
       | `Proof p -> 
-           (match  p.Con.proof_name with
-              Some "w" -> prerr_endline ("processing w");
-            | _ -> ());
            proof2pres p 
       | `Definition d -> 
            (match d.Con.def_name with