X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicPp.ml;h=9242d1fedab60a2fc4630f835a6c2685234754dd;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=7765328523669ca3ee088371addd99248d14481c;hpb=c0ea287ec40615f72fec8a900ce2e9eb3d23c301;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
index 776532852..9242d1fed 100644
--- 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
@@ -283,8 +295,8 @@ let is_prefix prefix string =
   if len <= len1 then
     begin
       let head = String.sub string 0 len in
-      if ((String.compare head prefix)=0) ||
-      ((String.compare head (String.lowercase prefix))=0) then 
+      if 
+      (String.compare (String.lowercase head) (String.lowercase prefix)=0) then 
 	begin
 	  let diff = len1-len in
 	  let tail = String.sub string len diff in
@@ -297,6 +309,11 @@ let is_prefix prefix string =
   else None
 
 let remove_prefix prefix (last,string) =
+  if prefix="append" then
+    begin 
+      prerr_endline last;
+      prerr_endline string;
+    end;
   if string = "" then (last,string)
   else 
     match is_prefix prefix string with
@@ -440,6 +457,8 @@ let rec check_names ctx hyp_names conclusion_name t =
 	hyp_names=[] && check_name ~allow_suffix:true ctx conclusion_name t
 
 let check name term =
+(*  prerr_endline name;
+  prerr_endline (ppterm term); *)
   let names = Str.split (Str.regexp_string "_to_") name in
   let hyp_names,conclusion_name =
     match List.rev names with