An exception was raised when a MutInd or MutConstruct had an uri to a

non-existing object. The whole URI + XPointer is now printed.

diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
index 05c964370b7b711941fc1a9a0930851058f60a37..30b91760dca74f278cf4a2da4804104c80ccee3e 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -107,19 +107,27 @@ let rec pp t l =
     | C.Const (uri,exp_named_subst) ->
        UriManager.name_of_uri uri ^ pp_exp_named_subst exp_named_subst l
     | C.MutInd (uri,n,exp_named_subst) ->
-       (match CicEnvironment.get_obj uri with
-           C.InductiveDefinition (dl,_,_) ->
-            let (name,_,_,_) = get_nth dl (n+1) in
-             name ^ pp_exp_named_subst exp_named_subst l
-         | _ -> raise CicPpInternalError
+       (try
+         match CicEnvironment.get_obj uri with
+            C.InductiveDefinition (dl,_,_) ->
+             let (name,_,_,_) = get_nth dl (n+1) in
+              name ^ pp_exp_named_subst exp_named_subst l
+          | _ -> raise CicPpInternalError
+        with
+         _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int n 
        )
     | C.MutConstruct (uri,n1,n2,exp_named_subst) ->
-       (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 ^ pp_exp_named_subst exp_named_subst l
-         | _ -> raise CicPpInternalError
+       (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 ^ pp_exp_named_subst exp_named_subst l
+          | _ -> raise CicPpInternalError
+        with
+         _ ->
+          UriManager.string_of_uri uri ^ "#1/" ^ string_of_int n1 ^ "/" ^
+           string_of_int n2
        )
     | C.MutCase (uri,n1,ty,te,patterns) ->
        let connames =
@@ -172,18 +180,14 @@ let ppterm t =
  pp t []
 ;;
 
-(* ppinductiveType (typename, inductive, arity, cons) names                 *)
-(* pretty-prints a single inductive definition (typename, inductive, arity, *)
-(*  cons) where the cic terms in the inductive definition need to be        *)
-(*  evaluated in the environment names that is the list of typenames of the *)
-(*  mutual inductive definitions defined in the block of mutual inductive   *)
-(*  definitions to which this one belongs to                                *)
-let ppinductiveType (typename, inductive, arity, cons) names =
+(* ppinductiveType (typename, inductive, arity, cons)                       *)
+(* pretty-prints a single inductive definition                              *)
+(* (typename, inductive, arity, cons)                                       *)
+let ppinductiveType (typename, inductive, arity, cons) =
   (if inductive then "\nInductive " else "\nCoInductive ") ^ typename ^ ": " ^
-  (*CSC: bug found: was pp arity names ^ " =\n   " ^*)
   pp arity [] ^ " =\n   " ^
   List.fold_right
-   (fun (id,ty) i -> id ^ " : " ^ pp ty names ^ 
+   (fun (id,ty) i -> id ^ " : " ^ pp ty [] ^ 
     (if i = "" then "\n" else "\n | ") ^ i)
    cons ""
 ;;
@@ -239,6 +243,5 @@ let ppobj obj =
       "Parameters = " ^
        String.concat ";" (List.map UriManager.string_of_uri params) ^ "\n" ^
        "NParams = " ^ string_of_int nparams ^ "\n" ^
-       let names = List.rev (List.map (fun (n,_,_,_) -> Some (C.Name n)) l) in
-        List.fold_right (fun x i -> ppinductiveType x names ^ i) l ""
+        List.fold_right (fun x i -> ppinductiveType x ^ i) l ""
 ;;