- redesigned error and warning handling for libxslt

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

diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
index 07e306b0be83e167708dd4a05266205e166bbeb1..fce4e7f48633a6ecc1070b19798f5ebf9d3437cb 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -103,22 +103,34 @@ let rec pp t l =
         li ""
        ) ^ ")"
     | C.Const (uri,_) -> UriManager.name_of_uri uri
-    | C.Abst 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