Big commit to let Ferruccio try the merge_coercion patch.

[helm.git] / helm / ocaml / acic_content / cicNotationPp.ml

diff --git a/helm/ocaml/acic_content/cicNotationPp.ml b/helm/ocaml/acic_content/cicNotationPp.ml
index bf0f9ed4c911c4fb97dbcbca78c303cf034250bd..0813c732a53bc6146be6cb81b04f73dd957eea88 100644 (file)
--- 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) ->