From: Ferruccio Guidi Date: Sun, 6 Sep 2015 19:22:38 +0000 (+0000) Subject: - the `Implied attribute is now printed X-Git-Tag: make_still_working~697 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=99d00e4b45463e5d3289103e91adddf7303479ea;p=helm.git - the `Implied attribute is now printed [also the `Generated attribute is printed. is this ok?] --- diff --git a/matita/components/content/notationPp.ml b/matita/components/content/notationPp.ml index d19bce283..baf92236c 100644 --- a/matita/components/content/notationPp.ml +++ b/matita/components/content/notationPp.ml @@ -275,6 +275,11 @@ let pp_fields pp_term fields = pp_term ty) fields) +let string_of_source = function + | `Provided -> "" + | `Implied -> "implied " + | `Generated -> "generated " + let pp_obj pp_term = function | Ast.Inductive (params, types) -> let pp_constructors constructors = @@ -295,8 +300,9 @@ let pp_obj pp_term = function (pp_term typ) (pp_constructors constructors) in fst_typ_pp ^ String.concat "" (List.map pp_type tl)) - | Ast.Theorem (name, typ, body,(_,flavour,_)) -> - sprintf "%s %s:\n %s\n%s" + | Ast.Theorem (name, typ, body,(source, flavour, _)) -> + sprintf "%s%s %s:\n %s\n%s" + (string_of_source source) (NCicPp.string_of_flavour flavour) name (pp_term typ) @@ -306,7 +312,7 @@ let pp_obj pp_term = function | Ast.Record (params,name,ty,fields) -> "record " ^ name ^ " " ^ pp_params pp_term params ^ ": " ^ pp_term ty ^ " \\def {" ^ pp_fields pp_term fields ^ "\n}" - | Ast.LetRec (kind, definitions, _) -> + | Ast.LetRec (kind, definitions, (source, _, _)) -> let rec get_guard i = function | [] -> assert false (* Ast.Implicit `JustOne *) | [term, _] when i = 1 -> term @@ -324,7 +330,8 @@ let pp_obj pp_term = function (pp_term (get_guard i params)) (pp_term typ) (pp_term body) in - sprintf "let %s %s" + sprintf "%slet %s %s" + (string_of_source source) (match kind with `Inductive -> "rec" | `CoInductive -> "corec") (String.concat " and " (List.map map definitions))