X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Facic_content%2FcicNotationPp.ml;h=2873912c0129d51b9b17e9a6f2f3aae80c144797;hb=e134b6f156268364d3027e73910c19e9c7e09838;hp=6d70c22c98ef09e80f5bb52e685fea06f4eef762;hpb=d32606924ee81fe309d016df7704f2612ebdc05e;p=helm.git

diff --git a/components/acic_content/cicNotationPp.ml b/components/acic_content/cicNotationPp.ml
index 6d70c22c9..2873912c0 100644
--- a/components/acic_content/cicNotationPp.ml
+++ b/components/acic_content/cicNotationPp.ml
@@ -263,6 +263,7 @@ let pp_params pp_term = function
       
 let pp_flavour = function
   | `Definition -> "definition"
+  | `MutualDefinition -> assert false
   | `Fact -> "fact"
   | `Goal -> "goal"
   | `Lemma -> "lemma"
@@ -301,6 +302,8 @@ let pp_obj pp_term = function
             (pp_term typ) (pp_constructors constructors)
         in
         fst_typ_pp ^ String.concat "" (List.map pp_type tl))
+ | Ast.Theorem (`MutualDefinition, name, typ, body) ->
+    sprintf "<<pretty printing of mutual definitions not implemented yet>>"
  | Ast.Theorem (flavour, name, typ, body) ->
     sprintf "%s %s:\n %s\n%s"
       (pp_flavour flavour)