X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicPp.ml;h=49d004ee0201d765c6a9445c172d38f24294091b;hb=31851952e1cc2db59168c5fd6f6093d9bc37ea86;hp=b0e7d64ed31be5f58e6c3c095b29eac6a845ee70;hpb=e626927b4c1c77bdcd6b545203a0a9c17a9ff136;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
index b0e7d64ed..49d004ee0 100644
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -85,7 +85,7 @@ let rec pp t l =
        (match s with
            C.Prop  -> "Prop"
          | C.Set   -> "Set"
-         | C.Type  -> "Type"
+         | C.Type _ -> "Type" (* TASSI: universe is not explicit *)
 	 | C.CProp -> "CProp" 
        )
     | C.Implicit _ -> "?"
@@ -109,7 +109,7 @@ let rec pp t l =
        UriManager.name_of_uri uri ^ pp_exp_named_subst exp_named_subst l
     | C.MutInd (uri,n,exp_named_subst) ->
        (try
-         match CicEnvironment.get_obj uri with
+         match fst(CicEnvironment.get_obj uri CicUniv.empty_ugraph) with
             C.InductiveDefinition (dl,_,_) ->
              let (name,_,_,_) = get_nth dl (n+1) in
               name ^ pp_exp_named_subst exp_named_subst l
@@ -119,7 +119,7 @@ let rec pp t l =
        )
     | C.MutConstruct (uri,n1,n2,exp_named_subst) ->
        (try
-         match CicEnvironment.get_obj uri with
+         match fst(CicEnvironment.get_obj uri CicUniv.empty_ugraph) with
             C.InductiveDefinition (dl,_,_) ->
              let (_,_,_,cons) = get_nth dl (n1+1) in
               let (id,_) = get_nth cons n2 in
@@ -132,7 +132,7 @@ let rec pp t l =
        )
     | C.MutCase (uri,n1,ty,te,patterns) ->
        let connames =
-        (match CicEnvironment.get_obj uri with
+        (match fst(CicEnvironment.get_obj uri CicUniv.empty_ugraph) with
             C.InductiveDefinition (dl,_,_) ->
              let (_,_,_,cons) = get_nth dl (n1+1) in
               List.map (fun (id,_) -> id) cons
@@ -193,6 +193,24 @@ let ppinductiveType (typename, inductive, arity, cons) =
    cons ""
 ;;
 
+let ppcontext ?(sep = "\n") context =
+ let separate s = if s = "" then "" else s ^ sep in
+ fst (List.fold_right 
+   (fun context_entry (i,name_context) ->
+     match context_entry with
+        Some (n,Cic.Decl t) ->
+         Printf.sprintf "%s%s : %s" (separate i) (ppname n)
+          (pp t name_context), (Some n)::name_context
+      | Some (n,Cic.Def (bo,ty)) ->
+         Printf.sprintf "%s%s : %s := %s" (separate i) (ppname n)
+          (match ty with
+              None -> "_"
+            | Some ty -> pp ty name_context)
+          (pp bo name_context), (Some n)::name_context
+       | None ->
+          Printf.sprintf "%s_ :? _" (separate i), None::name_context
+    ) context ("",[]))
+
 (* ppobj obj  returns a string with describing the cic object obj in a syntax *)
 (* similar to the one used by Coq                                             *)
 let ppobj obj =