X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationPp.ml;h=785c8bd8687794049dbd0000cf57685580378880;hb=b05fae519ae04a4a5dc79108f3d4ebe1bd4e112d;hp=cdc0946e6f96bd2d992984bd1043ffc3a7aa9932;hpb=2647a6b8df8fd913b05e33ef8606197cae825281;p=helm.git

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index cdc0946e6..785c8bd86 100644
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -122,7 +122,7 @@ let rec pp_term ?(pp_parens = true) t =
 	   aux i [] t
 	in
 	let rec get_guard i = function
-	   | []                   -> assert false
+	   | []                   -> (*assert false*) Ast.Implicit
 	   | [term, _] when i = 1 -> term
 	   | _ :: tl              -> get_guard (pred i) tl
 	in
@@ -132,7 +132,10 @@ let rec pp_term ?(pp_parens = true) t =
 	         let pvars, pbody = strip i typ in
 		 let _, bbody = strip i body in
 		 term, pvars, pbody, bbody
-	      | _              -> assert false
+	      | term, None ->
+                 let pbody = Ast.Implicit in
+		 let pvars, bbody = strip i body in
+		 term, pvars, pbody, bbody
 	   in
 	   sprintf "%s %s on %s: %s \\def %s" 
 	      (pp_term ~pp_parens:false term)
@@ -289,8 +292,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) ->