| 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
| [] -> ""
| `Remark -> "remark"
| `Theorem -> "theorem"
| `Variant -> "variant"
+ | `Axiom -> "axiom"
let pp_fields fields =
(if fields <> [] then "\n" else "") ^