...

[helm.git] / components / cic_proof_checking / cicPp.ml

diff --git a/components/cic_proof_checking/cicPp.ml b/components/cic_proof_checking/cicPp.ml
index 55d94899bc1b95ddae34462f38da2848775a4886..8c37c0f939f8aeed9d0f29999c7b8233f88f5147 100644 (file)
--- a/components/cic_proof_checking/cicPp.ml
+++ b/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 =