From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 9 Oct 2002 15:09:45 +0000 (+0000)
Subject: Pretty-printing of MUTIND and MUTCONSTRUCT with crazy indexes fixed.
X-Git-Tag: BEFORE_METADATA_FOR_SORT_AND_REL~44
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=93a4443fdbe05801da25d5df5dbef58610f93d92;p=helm.git

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 d34bbb5df..fce4e7f48 100644
--- 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