| C.Implicit _ -> "?"
| C.Prod (b,s,t) ->
(match b with
- C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t ((Some b)::l)
- | C.Anonymous -> "(" ^ pp s l ^ "->" ^ pp t ((Some b)::l) ^ ")"
+ C.Name n -> "(\forall " ^ n ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")"
+ | C.Anonymous -> "(" ^ pp s l ^ "\\to " ^ pp t ((Some b)::l) ^ ")"
)
| C.Cast (v,t) -> "(" ^ pp v l ^ ":" ^ pp t l ^ ")"
| C.Lambda (b,s,t) ->
"(\\lambda " ^ ppname b ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")"
| C.LetIn (b,s,t) ->
- "[" ^ ppname b ^ ":=" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
+ " let " ^ ppname b ^ " \def " ^ pp s l ^ " in " ^ pp t ((Some b)::l)
| C.Appl li ->
"(" ^
(List.fold_right
name ^ pp_exp_named_subst exp_named_subst l
| _ -> raise CicPpInternalError
with
- _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
+ Sys.Break as exn -> raise exn
+ | _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
)
| C.MutConstruct (uri,n1,n2,exp_named_subst) ->
(try
id ^ pp_exp_named_subst exp_named_subst l
| _ -> raise CicPpInternalError
with
- _ ->
+ Sys.Break as exn -> raise exn
+ | _ ->
UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^
string_of_int n2
)
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