Bug fixed: Invalid_argument was raised by List.combine in place of a typing

[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 7765328523669ca3ee088371addd99248d14481c..93d7d0a04b03d1fe7e1e532ba9cf5570198cf864 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -141,9 +141,21 @@ let rec pp t l =
           | _ -> raise CicPpInternalError
         )
        in
+        let connames_and_patterns =
+         let rec combine =
+            function
+               [],[] -> []
+             | [],l -> List.map (fun x -> "???",Some x) l
+             | l,[] -> List.map (fun x -> x,None) l
+             | x::tlx,y::tly -> (x,Some y)::(combine (tlx,tly))
+         in
+          combine (connames,patterns)
+        in
         "\n<" ^ pp ty l ^ ">Cases " ^ pp te l ^ " of " ^
-          List.fold_right (fun (x,y) i -> "\n " ^ x ^ " => " ^ pp y l ^ i)
-           (List.combine connames patterns) "" ^
+          List.fold_right
+           (fun (x,y) i -> "\n " ^ x ^ " => " ^
+             (match y with None -> "" | Some y -> pp y l) ^ i)
+           connames_and_patterns "" ^
           "\nend"
     | C.Fix (no, funs) ->
        let snames = List.map (fun (name,_,_,_) -> name) funs in