Capturing Invalid_argument inside pp (otherwise we cannot even

see what's wrong *) wrong.

diff --git a/helm/software/components/cic_proof_checking/cicPp.ml b/helm/software/components/cic_proof_checking/cicPp.ml
index 55d94899bc1b95ddae34462f38da2848775a4886..d065ee74a0d04c4d13a0f40dd6372d92c0dadcb8 100644 (file)
--- 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
                     ) 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) ^
               "???" ^ (string_of_int n) ^ "[" ^ 
                String.concat " ; "
                 (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^