* Major code cleanup.

[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 fafbd884845ee5465d555860647eed8002fa24e0..97ae6a50f5b8f189f6bc11fe8f145e1a1f3fbe20 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -37,6 +37,7 @@
 (******************************************************************************)
 
 exception CicPpInternalError;;
+exception NotEnoughElements;;
 
 (* Utility functions *)
 
@@ -46,13 +47,13 @@ let string_of_name =
   | Cic.Anonimous  -> "_"
 ;;
 
-(* get_nth l n   returns the nth element of the list l if it exists or raise *)
-(* a CicPpInternalError if l has less than n elements or n < 1               *)
+(* get_nth l n   returns the nth element of the list l if it exists or *)
+(* raises NotEnoughElements if l has less than n elements             *)
 let rec get_nth l n =
  match (n,l) with
     (1, he::_) -> he
   | (n, he::tail) when n > 1 -> get_nth tail (n-1)
-  | (_,_) -> raise CicPpInternalError
+  | (_,_) -> raise NotEnoughElements
 ;;
 
 (* pp t l                                                                  *)
@@ -63,10 +64,15 @@ let rec pp t l =
  let module C = Cic in
    match t with
       C.Rel n ->
-       (match get_nth l n with
-           C.Name s -> s
-         | _        -> raise CicPpInternalError
-       )
+       begin
+        try
+         (match get_nth l n with
+             C.Name s -> s
+           | _        -> raise CicPpInternalError
+         )
+        with
+         NotEnoughElements -> string_of_int (List.length l - n)
+       end
     | C.Var uri -> UriManager.name_of_uri uri
     | C.Meta n -> "?" ^ (string_of_int n)
     | C.Sort s ->