and pp_patterns patterns =
sprintf "[%s]" (String.concat " | " (List.map pp_pattern patterns))
-and pp_capture_variable = function
+and pp_capture_variable =
+ let clean s =
+ let s = String.sub s 1 (String.length s - 1) in
+ String.sub s 0 (String.length s - 1)
+ in
+ function
| term, None -> pp_term term
- | term, Some typ -> "(" ^ pp_term term ^ ": " ^ pp_term typ ^ ")"
+ | term, Some typ -> "(" ^ clean (pp_term term) ^ ": " ^ pp_term typ ^ ")"
and pp_box_spec (kind, spacing, indent) =
let int_of_bool b = if b then 1 else 0 in
| Ast.Ascription (t, n) -> assert false
| Ast.FreshVar n -> "fresh " ^ n
-let pp_term t = pp_term ~pp_parens:false t
+let _pp_term = ref (pp_term ~pp_parens:false)
+let pp_term t = !_pp_term t
+let set_pp_term f = _pp_term := f
let pp_params = function
| [] -> ""
let pp_flavour = function
| `Definition -> "Definition"
- | `Fact -> "Fact"
- | `Goal -> "Goal"
- | `Lemma -> "Lemma"
- | `Remark -> "Remark"
- | `Theorem -> "Theorem"
- | `Variant -> "Variant"
+ | `Fact -> "fact"
+ | `Goal -> "goal"
+ | `Lemma -> "lemma"
+ | `Remark -> "remark"
+ | `Theorem -> "theorem"
+ | `Variant -> "variant"
+ | `Axiom -> "axiom"
let pp_fields fields =
(if fields <> [] then "\n" else "") ^