(pp_patterns patterns)
| Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term ~pp_parens:true t1) (pp_term ~pp_parens:true t2)
| Ast.LetIn ((var,t2), t1, t3) ->
- let t2 = match t2 with None -> Ast.Implicit | Some t -> t in
- sprintf "let %s : %s \\def %s in %s" (pp_term var)
- (pp_term ~pp_parens:true t2)
+(* let t2 = match t2 with None -> Ast.Implicit | Some t -> t in *)
+ sprintf "let %s \\def %s in %s" (pp_term var)
+(* (pp_term ~pp_parens:true t2) *)
(pp_term ~pp_parens:true t1)
(pp_term ~pp_parens:true t3)
| Ast.LetRec (kind, definitions, term) ->
| Ast.Sort `Set -> "Set"
| Ast.Sort `Prop -> "Prop"
| Ast.Sort (`Type _) -> "Type"
- | Ast.Sort `CProp -> "CProp"
+ | Ast.Sort (`CProp _)-> "CProp"
| Ast.Symbol (name, _) -> "'" ^ name
| Ast.UserInput -> ""