CSC: tentative definition of the ocaml structure that represents

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

diff --git a/helm/ocaml/cic_transformations/contentPp.ml b/helm/ocaml/cic_transformations/contentPp.ml
index 4206404f5ca1cfeb6c281df6d3f8290f5cd5446a..e42c987901fc7b7fded07eaff3e9077c86971d70 100644 (file)
--- a/helm/ocaml/cic_transformations/contentPp.ml
+++ b/helm/ocaml/cic_transformations/contentPp.ml
@@ -34,6 +34,7 @@
 
 exception ContentPpInternalError;;
 exception NotEnoughElements;;
+exception TO_DO
 
 (* Utility functions *)
 
@@ -57,7 +58,7 @@ let rec blanks n =
   if n = 0 then ""
   else (" " ^ (blanks (n-1)));; 
 
-let rec pproof p indent =
+let rec pproof (p: Cic.annterm Cic2content.proof) indent =
   let module Con = Cic2content in
   let new_indent =
     (match p.Con.proof_name with
@@ -78,7 +79,7 @@ and pcontext c indent =
 and pcontext_element indent =
   let module Con = Cic2content in
   function
-      Con.Declaration d -> 
+      `Declaration d -> 
         (match d.Con.dec_name with
             Some s -> 
               prerr_endline 
@@ -88,7 +89,7 @@ and pcontext_element indent =
               flush stderr
           | None ->
               prerr_endline ((blanks indent) ^ "NO NAME!!"))
-    | Con.Hypothesis h ->
+    | `Hypothesis h ->
          (match h.Con.dec_name with
             Some s -> 
               prerr_endline 
@@ -98,8 +99,8 @@ and pcontext_element indent =
               flush stderr
           | None ->
               prerr_endline ((blanks indent) ^ "NO NAME!!"))
-    | Con.Proof p -> pproof p indent
-    | Con.Definition d -> 
+    | `Proof p -> pproof p indent
+    | `Definition d -> 
          (match d.Con.def_name with
             Some s -> 
               prerr_endline 
@@ -108,7 +109,7 @@ and pcontext_element indent =
               flush stderr
           | None ->
               prerr_endline ((blanks indent) ^ "NO NAME!!")) 
-    | Con.Joint ho -> 
+    | `Joint ho -> 
          prerr_endline ((blanks indent) ^ "Joint Def");
          flush stderr
 
@@ -136,9 +137,10 @@ and parg indent =
         flush stderr
     | Con.ArgProof p -> pproof p (indent+1) 
     | Con.ArgMethod s -> prerr_endline ((blanks (indent+1)) ^ "A Method !!!");flush stderr
-
 ;;
  
 let print_proof p = pproof p 0;
 
 
+
+