X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent%2FnotationPp.ml;h=038d75d9c7afd1862bfc0909ee002fd019d158b6;hb=ae88c7c1481ac9ddf5d55e2144b6db418a25fdd1;hp=49002d108191b8baa7df13f033e24898c068c705;hpb=5832735b721c0bd8567c8f0be761a9136363a2a6;p=helm.git diff --git a/matita/components/content/notationPp.ml b/matita/components/content/notationPp.ml index 49002d108..038d75d9c 100644 --- a/matita/components/content/notationPp.ml +++ b/matita/components/content/notationPp.ml @@ -110,7 +110,7 @@ let rec pp_term (status : #NCic.status) ?(pp_parens = true) t = (match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t)) (pp_patterns status patterns) | Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term ~pp_parens:true t1) (pp_term ~pp_parens:true t2) - | Ast.LetIn ((var,t2), t1, t3) -> + | Ast.LetIn ((var,_t2), t1, t3) -> (* let t2 = match t2 with None -> Ast.Implicit | Some t -> t in *) sprintf "let %s \\def %s in %s" (pp_term var) (* (pp_term ~pp_parens:true t2) *) @@ -251,8 +251,8 @@ and pp_variable = function | Ast.NumVar s -> "number " ^ s | Ast.IdentVar s -> "ident " ^ s | Ast.TermVar (s,Ast.Self _) -> s - | Ast.TermVar (s,Ast.Level l) -> "term " ^string_of_int l - | Ast.Ascription (t, n) -> assert false + | Ast.TermVar (_s,Ast.Level l) -> "term " ^string_of_int l + | Ast.Ascription (_t, _n) -> assert false | Ast.FreshVar n -> "fresh " ^ n let _pp_term = ref (pp_term ~pp_parens:false) @@ -314,7 +314,7 @@ let pp_obj pp_term = function string_of_source source ^ "record " ^ name ^ " " ^ pp_params pp_term params ^ ": " ^ pp_term ty ^ " \\def {" ^ pp_fields pp_term fields ^ "\n}" - | Ast.LetRec (kind, definitions, (source, _, _)) -> + | Ast.LetRec (kind, definitions, (source, flavour, _)) -> let rec get_guard i = function | [] -> assert false (* Ast.Implicit `JustOne *) | [term, _] when i = 1 -> term @@ -332,9 +332,10 @@ let pp_obj pp_term = function (pp_term (get_guard i params)) (pp_term typ) (pp_term body) in - sprintf "%slet %s %s" + sprintf "%s%s %s %s" (string_of_source source) (match kind with `Inductive -> "rec" | `CoInductive -> "corec") + (NCicPp.string_of_flavour flavour) (String.concat " and " (List.map map definitions)) let rec pp_value (status: #NCic.status) = function