- Lemma added to the list of proof arguments

[helm.git] / helm / ocaml / cic_omdoc / contentPp.ml

diff --git a/helm/ocaml/cic_omdoc/contentPp.ml b/helm/ocaml/cic_omdoc/contentPp.ml
index b51cba99d384c144fdc6861155063fdedb62964a..58ba4873b627bbed8d3bd7aef47ff0a2e815c500 100644 (file)
--- a/helm/ocaml/cic_omdoc/contentPp.ml
+++ b/helm/ocaml/cic_omdoc/contentPp.ml
@@ -130,13 +130,13 @@ and pargs args indent =
 and parg indent =
   let module Con = Content in
   function
-       Con.Aux n ->  prerr_endline ((blanks (indent+1)) ^ n);flush stderr
-    |  Con.Premise prem -> prerr_endline ((blanks (indent+1)) ^ "Premise");flush stderr
+      Con.Aux n ->  prerr_endline ((blanks (indent+1)) ^ n)
+    | Con.Premise prem -> prerr_endline ((blanks (indent+1)) ^ "Premise")
+    | Con.Lemma lemma -> prerr_endline ((blanks (indent+1)) ^ "Lemma")
     | Con.Term t -> 
-        prerr_endline ((blanks (indent+1)) ^ (CicPp.ppterm (Deannotate.deannotate_term t)));
-        flush stderr
+        prerr_endline ((blanks (indent+1)) ^ (CicPp.ppterm (Deannotate.deannotate_term t)))
     | Con.ArgProof p -> pproof p (indent+1) 
-    | Con.ArgMethod s -> prerr_endline ((blanks (indent+1)) ^ "A Method !!!");flush stderr
+    | Con.ArgMethod s -> prerr_endline ((blanks (indent+1)) ^ "A Method !!!")
 ;;
  
 let print_proof p = pproof p 0;