X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationPp.ml;h=2873912c0129d51b9b17e9a6f2f3aae80c144797;hb=5d1cece5f42866b34566a0f616aa3b46a77359a3;hp=6d70c22c98ef09e80f5bb52e685fea06f4eef762;hpb=4609a07e2fe4343d94832fcaf0936223f83ba71c;p=helm.git

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index 6d70c22c9..2873912c0 100644
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/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)