From 93a4443fdbe05801da25d5df5dbef58610f93d92 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 9 Oct 2002 15:09:45 +0000 Subject: [PATCH] Pretty-printing of MUTIND and MUTCONSTRUCT with crazy indexes fixed. --- helm/ocaml/cic_proof_checking/cicPp.ml | 39 +++++++++++++++++--------- 1 file changed, 26 insertions(+), 13 deletions(-) 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 -- 2.39.2