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=ff0a09265c0d6b985d4c439b70931f74f0b8eb0a;hpb=873f8a47b13fbf07df383f3b95d0f4994d2ce136;p=helm.git diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml index ff0a09265..785c8bd86 100644 --- a/helm/software/components/acic_content/cicNotationPp.ml +++ b/helm/software/components/acic_content/cicNotationPp.ml @@ -99,7 +99,6 @@ let rec pp_term ?(pp_parens = true) t = | Ast.Case (term, indtype, typ, patterns) -> sprintf "match %s%s%s with %s" (pp_term term) - (match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t)) (match indtype with | None -> "" | Some (ty, href_opt) -> @@ -107,7 +106,8 @@ let rec pp_term ?(pp_parens = true) t = (match debug_printing, href_opt with | true, Some uri -> sprintf "(i.e.%s)" (UriManager.string_of_uri uri) - | _ -> "")) + | _ -> "")) + (match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t)) (pp_patterns patterns) | Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term ~pp_parens:true t1) (pp_term ~pp_parens:true t2) | Ast.LetIn (var, t1, t2) -> @@ -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) ->