X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Facic_content%2FcicNotationPp.ml;h=5dc6fd821c380f311a37005d5ed5057af33b2352;hb=ee8a9f2a9f75814be05fa9f7aafefb3e42692a2a;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..5dc6fd821 100644
--- a/helm/ocaml/acic_content/cicNotationPp.ml
+++ b/helm/ocaml/acic_content/cicNotationPp.ml
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 open Printf
 
 module Ast = CicNotationPt
@@ -255,7 +257,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) ->