Changed auto from implicit to option and renamed a few functions.

[helm.git] / helm / software / components / acic_content / cicNotationPp.ml

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index cdc0946e6f96bd2d992984bd1043ffc3a7aa9932..785c8bd8687794049dbd0000cf57685580378880 100644 (file)
--- 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) ->