X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Facic_content%2FcicNotationPp.ml;h=5f45b2a4ba72d23ea6f942d6124357578f3b2508;hb=b09b0e4b30c429d8e050150cc4e9b94d7c205368;hp=590de7c5462f4fe5b097113f19ff20133da23a5d;hpb=4cdf45f08cd95641a094312ddc558320b874fa16;p=helm.git

diff --git a/components/acic_content/cicNotationPp.ml b/components/acic_content/cicNotationPp.ml
index 590de7c54..5f45b2a4b 100644
--- a/components/acic_content/cicNotationPp.ml
+++ b/components/acic_content/cicNotationPp.ml
@@ -239,7 +239,9 @@ and pp_variable = function
   | 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
   | [] -> ""
@@ -258,6 +260,7 @@ let pp_flavour = function
   | `Remark -> "remark"
   | `Theorem -> "theorem"
   | `Variant -> "variant"
+  | `Axiom -> "axiom"
 
 let pp_fields fields =
   (if fields <> [] then "\n" else "") ^