X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Facic_content%2FcicNotationPp.ml;h=0813c732a53bc6146be6cb81b04f73dd957eea88;hb=7d7f729471b4d5ebafa1b915096974e726cc13c6;hp=bf0f9ed4c911c4fb97dbcbca78c303cf034250bd;hpb=9a0e4f3be9f70662f18d2d3b6dd60ae79fba565b;p=helm.git

diff --git a/helm/ocaml/acic_content/cicNotationPp.ml b/helm/ocaml/acic_content/cicNotationPp.ml
index bf0f9ed4c..0813c732a 100644
--- a/helm/ocaml/acic_content/cicNotationPp.ml
+++ b/helm/ocaml/acic_content/cicNotationPp.ml
@@ -255,7 +255,9 @@ let pp_flavour = function
 let pp_fields fields =
   (if fields <> [] then "\n" else "") ^ 
   String.concat ";\n" 
-    (List.map (fun (name,ty) -> " " ^ name ^ ": " ^ pp_term ty) fields)
+    (List.map 
+      (fun (name,ty,coercion) -> 
+        " " ^ name ^ if coercion then ":>" else ": " ^ pp_term ty) fields)
         
 let pp_obj = function
  | Ast.Inductive (params, types) ->