X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicPp.ml;h=97213404e7244a0b8c082b68b44f1d12bf14d53c;hb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;hp=55d94899bc1b95ddae34462f38da2848775a4886;hpb=7e30c63fcf9f9fe1780ba7aa4d95fd0d8658548b;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicPp.ml b/helm/software/components/cic_proof_checking/cicPp.ml
index 55d94899b..97213404e 100644
--- a/helm/software/components/cic_proof_checking/cicPp.ml
+++ b/helm/software/components/cic_proof_checking/cicPp.ml
@@ -101,7 +101,8 @@ let rec pp t l =
                     ) context l1)) ^
                "]"
             with
-             CicUtil.Meta_not_found _ ->
+	      CicUtil.Meta_not_found _ 
+            | Invalid_argument _ ->
               "???" ^ (string_of_int n) ^ "[" ^ 
                String.concat " ; "
                 (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
@@ -113,7 +114,7 @@ let rec pp t l =
          | C.Set   -> "Set"
          | C.Type _ -> "Type"
          (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
-	 | C.CProp -> "CProp" 
+	 | C.CProp _ -> "CProp" 
        )
     | C.Implicit (Some `Hole) -> "%"
     | C.Implicit _ -> "?"
@@ -125,8 +126,8 @@ let rec pp t l =
     | C.Cast (v,t) -> "(" ^ pp v l ^ ":" ^ pp t l ^ ")"
     | C.Lambda (b,s,t) ->
        "(\\lambda " ^ ppname b ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")"
-    | C.LetIn (b,s,t) ->
-       " let " ^ ppname b ^ " \\def " ^ pp s l ^ " in " ^ pp t ((Some b)::l)
+    | C.LetIn (b,s,ty,t) ->
+       " let " ^ ppname b ^ ": " ^ pp ty l ^ " \\def " ^ pp s l ^ " in " ^ pp t ((Some b)::l)
     | C.Appl li ->
        "(" ^
        (List.fold_right
@@ -166,7 +167,7 @@ let rec pp t l =
             C.InductiveDefinition (dl,_,paramsno,_) ->
              let (_,_,_,cons) = get_nth dl (n1+1) in
               List.map
-               (fun id,ty ->
+               (fun (id,ty) ->
                  (* this is just an approximation since we do not have
                     reduction yet! *)
                  let rec count_prods toskip =
@@ -277,9 +278,7 @@ let ppcontext ?metasenv ?(sep = "\n") context =
           (pp ?metasenv 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 ?metasenv ty name_context)
+          (pp ?metasenv ty name_context)
           (pp ?metasenv bo name_context), (Some n)::name_context
        | None ->
           Printf.sprintf "%s_ :? _" (separate i), None::name_context
@@ -317,18 +316,19 @@ let ppobj obj =
 	          (fun context_entry (i,name_context) ->
 	            (match context_entry with
 	                Some (n,C.Decl at) ->
-                   (separate i) ^
-                     ppname n ^ ":" ^
-                      pp ~metasenv:conjectures at name_context ^ " ",
-                      (Some n)::name_context
-	              | Some (n,C.Def (at,None)) ->
-                   (separate i) ^
-                     ppname n ^ ":= " ^ pp ~metasenv:conjectures
-                      at name_context ^ " ",
-                      (Some n)::name_context
-                | None ->
-                   (separate i) ^ "_ :? _ ", None::name_context
-                | _ -> assert false)
+                         (separate i) ^
+                           ppname n ^ ":" ^
+                            pp ~metasenv:conjectures at name_context ^ " ",
+                            (Some n)::name_context
+                      | Some (n,C.Def (at,aty)) ->
+                         (separate i) ^
+                           ppname n ^ ": " ^
+                            pp ~metasenv:conjectures aty name_context ^
+                            ":= " ^ pp ~metasenv:conjectures
+                            at name_context ^ " ",
+                            (Some n)::name_context
+                      | None ->
+                         (separate i) ^ "_ :? _ ", None::name_context)
             ) context ("",[])
           in
            conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
@@ -347,7 +347,7 @@ let ppsort = function
   | Cic.Prop -> "Prop"
   | Cic.Set -> "Set"
   | Cic.Type _ -> "Type"
-  | Cic.CProp -> "CProp"
+  | Cic.CProp _ -> "CProp"
 
 
 (* MATITA NAMING CONVENTION *)
@@ -412,7 +412,7 @@ let rec check_rec ctx string_name =
     | Cic.Cast (te,ty) -> check_rec ctx string_name te
     | Cic.Prod (name,so,dest) -> 
 	let l_string_name = check_rec ctx string_name so in
-	check_rec (name::ctx) string_name dest
+	check_rec (name::ctx) l_string_name dest
     | Cic.Lambda (name,so,dest) -> 
         let string_name =
           match name with
@@ -420,7 +420,7 @@ let rec check_rec ctx string_name =
           | Cic.Name name -> remove_prefix name string_name in
         let l_string_name = check_rec ctx string_name so in
 	check_rec (name::ctx) l_string_name dest
-    | Cic.LetIn (name,so,dest) -> 
+    | Cic.LetIn (name,so,_,dest) -> 
         let string_name = check_rec ctx string_name so in
 	check_rec (name::ctx) string_name dest
     | Cic.Appl l ->