Pretty-printing of MUTIND and MUTCONSTRUCT with crazy indexes fixed.

diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
index d34bbb5df2f68a9c5f20c4f329bfe134960ded62..fce4e7f48633a6ecc1070b19798f5ebf9d3437cb 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -104,20 +104,33 @@ let rec pp t l =
        ) ^ ")"
     | C.Const (uri,_) -> UriManager.name_of_uri uri
     | C.MutInd (uri,_,n) ->
-       (match CicEnvironment.get_obj uri with
-           C.InductiveDefinition (dl,_,_) ->
-            let (name,_,_,_) = get_nth dl (n+1) in
-             name
-         | _ -> raise CicPpInternalError
-       )
+       begin
+        try
+         (match CicEnvironment.get_obj uri with
+             C.InductiveDefinition (dl,_,_) ->
+              let (name,_,_,_) = get_nth dl (n+1) in
+               name
+           | _ -> raise CicPpInternalError
+         )
+        with
+         NotEnoughElements ->
+          UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
+       end
     | C.MutConstruct (uri,_,n1,n2) ->
-       (match CicEnvironment.get_obj uri with
-           C.InductiveDefinition (dl,_,_) ->
-            let (_,_,_,cons) = get_nth dl (n1+1) in
-             let (id,_,_) = get_nth cons n2 in
-              id
-         | _ -> raise CicPpInternalError
-       )
+       begin
+        try
+         (match CicEnvironment.get_obj uri with
+             C.InductiveDefinition (dl,_,_) ->
+              let (_,_,_,cons) = get_nth dl (n1+1) in
+               let (id,_,_) = get_nth cons n2 in
+                id
+           | _ -> raise CicPpInternalError
+         )
+        with
+         NotEnoughElements ->
+          UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^
+           string_of_int n2
+       end
     | C.MutCase (uri,_,n1,ty,te,patterns) ->
        let connames =
         (match CicEnvironment.get_obj uri with