| C.Set -> "Set"
| C.Type _ -> "Type"
(*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
- | C.CProp -> "CProp"
+ | C.CProp _ -> "CProp"
)
| C.Implicit (Some `Hole) -> "%"
| C.Implicit _ -> "?"
| 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) ->
- " let " ^ ppname b ^ " \\def " ^ pp s l ^ " in " ^ pp t ((Some b)::l)
+ | C.LetIn (b,s,ty,t) ->
+ " let " ^ ppname b ^ ": " ^ pp ty l ^ " \\def " ^ pp s l ^ " in " ^ pp t ((Some b)::l)
| C.Appl li ->
"(" ^
(List.fold_right
(pp ?metasenv t name_context), (Some n)::name_context
| Some (n,Cic.Def (bo,ty)) ->
Printf.sprintf "%s%s : %s := %s" (separate i) (ppname n)
- (match ty with
- None -> "_"
- | Some ty -> pp ?metasenv ty name_context)
+ (pp ?metasenv ty name_context)
(pp ?metasenv bo name_context), (Some n)::name_context
| None ->
Printf.sprintf "%s_ :? _" (separate i), None::name_context
(fun context_entry (i,name_context) ->
(match context_entry with
Some (n,C.Decl at) ->
- (separate i) ^
- ppname n ^ ":" ^
- pp ~metasenv:conjectures at name_context ^ " ",
- (Some n)::name_context
- | Some (n,C.Def (at,None)) ->
- (separate i) ^
- ppname n ^ ":= " ^ pp ~metasenv:conjectures
- at name_context ^ " ",
- (Some n)::name_context
- | None ->
- (separate i) ^ "_ :? _ ", None::name_context
- | _ -> assert false)
+ (separate i) ^
+ ppname n ^ ":" ^
+ pp ~metasenv:conjectures at name_context ^ " ",
+ (Some n)::name_context
+ | Some (n,C.Def (at,aty)) ->
+ (separate i) ^
+ ppname n ^ ": " ^
+ pp ~metasenv:conjectures aty name_context ^
+ ":= " ^ pp ~metasenv:conjectures
+ at name_context ^ " ",
+ (Some n)::name_context
+ | None ->
+ (separate i) ^ "_ :? _ ", None::name_context)
) context ("",[])
in
conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
| Cic.Prop -> "Prop"
| Cic.Set -> "Set"
| Cic.Type _ -> "Type"
- | Cic.CProp -> "CProp"
+ | Cic.CProp _ -> "CProp"
(* MATITA NAMING CONVENTION *)
| Cic.Name name -> remove_prefix name string_name in
let l_string_name = check_rec ctx string_name so in
check_rec (name::ctx) l_string_name dest
- | Cic.LetIn (name,so,dest) ->
+ | Cic.LetIn (name,so,_,dest) ->
let string_name = check_rec ctx string_name so in
check_rec (name::ctx) string_name dest
| Cic.Appl l ->