Several bugs fixed:

[helm.git] / components / acic_content / cicNotationPp.ml

diff --git a/components/acic_content/cicNotationPp.ml b/components/acic_content/cicNotationPp.ml
index 6d70c22c98ef09e80f5bb52e685fea06f4eef762..2873912c0129d51b9b17e9a6f2f3aae80c144797 100644 (file)
--- 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)