| _ -> 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
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
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
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