X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicPp.ml;h=8c37c0f939f8aeed9d0f29999c7b8233f88f5147;hb=947ee89dec9e60561dfac3ce7e1842f35f178cb8;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..8c37c0f93 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) ^ @@ -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 =