X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicPp.ml;h=11ed4418c67f8f4eae0f0244397306f45c62354e;hb=265cf771fbfe217b5f274b999fc3ad887683a09a;hp=d3f7f0f60b181f7ccdcc02de45176079e92300dc;hpb=edf601b6b8eb5b28a5292d0660a3b54b5680e580;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
index d3f7f0f60..11ed4418c 100644
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -220,20 +220,21 @@ let ppobj obj =
        List.fold_right
         (fun (n, context, t) i -> 
           let conjectures',name_context =
-	   List.fold_right 
-	    (fun context_entry (i,name_context) ->
-	      (match context_entry with
-	          Some (n,C.Decl at) ->
+	         List.fold_right 
+	          (fun context_entry (i,name_context) ->
+	            (match context_entry with
+	                Some (n,C.Decl at) ->
                    (separate i) ^
-                    string_of_name n ^ ":" ^ pp at name_context ^ " ",
-                   (Some n)::name_context
-	        | Some (n,C.Def at) ->
+                     string_of_name n ^ ":" ^ pp at name_context ^ " ",
+                      (Some n)::name_context
+	              | Some (n,C.Def (at,None)) ->
                    (separate i) ^
-                    string_of_name n ^ ":= " ^ pp at name_context ^ " ",
-                   (Some n)::name_context
+                     string_of_name n ^ ":= " ^ pp at name_context ^ " ",
+                      (Some n)::name_context
                 | None ->
-                   (separate i) ^ "_ :? _ ", None::name_context)
-             ) context ("",[])
+                   (separate i) ^ "_ :? _ ", None::name_context
+                | _ -> assert false)
+            ) context ("",[])
           in
            conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
             pp t name_context ^ "\n" ^ i