X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicPp.ml;h=fce4e7f48633a6ecc1070b19798f5ebf9d3437cb;hb=b1fb6b8e1767d775bc452303629e95941d142bea;hp=07e306b0be83e167708dd4a05266205e166bbeb1;hpb=37f08b2aba9f17d9d609ca0f57d607f437a3d3fc;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
index 07e306b0b..fce4e7f48 100644
--- 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