]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/acic_content/cicNotationPp.ml
Added a parameter (empty list) to load_notation.
[helm.git] / helm / ocaml / acic_content / cicNotationPp.ml
index bf0f9ed4c911c4fb97dbcbca78c303cf034250bd..5dc6fd821c380f311a37005d5ed5057af33b2352 100644 (file)
@@ -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) ->