]> matita.cs.unibo.it Git - helm.git/blobdiff - components/acic_content/cicNotationPp.ml
BIG FAT COMMIT REGARDING COERCIONS:
[helm.git] / components / acic_content / cicNotationPp.ml
index cdc0946e6f96bd2d992984bd1043ffc3a7aa9932..49cefaec7db3f7f76652d9e24e9543bd4de9f495 100644 (file)
@@ -289,8 +289,11 @@ let pp_fields fields =
   (if fields <> [] then "\n" else "") ^ 
   String.concat ";\n" 
     (List.map 
-      (fun (name,ty,coercion) -> 
-        " " ^ name ^ if coercion then ":>" else ": " ^ pp_term ty) fields)
+      (fun (name,ty,coercion,arity) -> 
+        " " ^ name ^ 
+        if coercion then (":" ^ 
+          if arity > 0 then string_of_int arity else "" ^ ">") else ": " ^
+        pp_term ty) fields)
         
 let pp_obj = function
  | Ast.Inductive (params, types) ->