X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent%2FnotationPp.ml;h=369a0fa281ac05e610f56d130b8cd477b4755724;hb=ab2f735d97d2b9c965f13527d5f6f61048d29b22;hp=49002d108191b8baa7df13f033e24898c068c705;hpb=c3904c007394068ed823575e3be3d73a9ad92cce;p=helm.git

diff --git a/matita/components/content/notationPp.ml b/matita/components/content/notationPp.ml
index 49002d108..369a0fa28 100644
--- a/matita/components/content/notationPp.ml
+++ b/matita/components/content/notationPp.ml
@@ -314,7 +314,7 @@ let pp_obj pp_term = function
     string_of_source source ^
     "record " ^ name ^ " " ^ pp_params pp_term params ^ ": " ^ pp_term ty ^ 
     " \\def {" ^ pp_fields pp_term fields ^ "\n}"
- | Ast.LetRec (kind, definitions, (source, _, _)) ->
+ | Ast.LetRec (kind, definitions, (source, flavour, _)) ->
     let rec get_guard i = function
        | []                   -> assert false (* Ast.Implicit `JustOne *)
        | [term, _] when i = 1 -> term
@@ -332,9 +332,10 @@ let pp_obj pp_term = function
 	  (pp_term (get_guard i params))
 	  (pp_term typ) (pp_term body)
     in
-    sprintf "%slet %s %s"
+    sprintf "%s%s %s %s"
       (string_of_source source)
       (match kind with `Inductive -> "rec" | `CoInductive -> "corec")
+      (NCicPp.string_of_flavour flavour)
       (String.concat " and " (List.map map definitions))
 
 let rec pp_value (status: #NCic.status) = function