X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent_pres%2FtermContentPres.ml;h=49d9241b96e8290ebef312443be7fa20811de9e3;hb=53b8e2af661ad4165aa0b1deccd0a7522d96ce2e;hp=4a65e6ec9595099b3ab2f8fc6e05a4e7648f2923;hpb=88a68a9c334646bc17314d5327cd3b790202acd6;p=helm.git diff --git a/matita/components/content_pres/termContentPres.ml b/matita/components/content_pres/termContentPres.ml index 4a65e6ec9..49d9241b9 100644 --- a/matita/components/content_pres/termContentPres.ml +++ b/matita/components/content_pres/termContentPres.ml @@ -214,6 +214,7 @@ let pp_ast0 status t k = ]; break; k t ]) +(* | Ast.LetRec (rec_kind, funs, where) -> let rec_op = match rec_kind with `Inductive -> "rec" | `CoInductive -> "corec" @@ -261,6 +262,7 @@ let pp_ast0 status t k = ((hvbox false false (fst_row :: List.flatten tl_rows @ [ break; keyword "in"; break; k where ]))) +*) | Ast.Implicit `JustOne -> builtin_symbol "?" | Ast.Implicit `Vector -> builtin_symbol "…" | Ast.Meta (n, l) -> @@ -594,9 +596,11 @@ let instantiate_level2 status env term = List.map (aux_branch env) patterns) | Ast.LetIn (var, t1, t3) -> Ast.LetIn (aux_capture_var env var, aux env t1, aux env t3) +(* | Ast.LetRec (kind, definitions, body) -> Ast.LetRec (kind, List.map (aux_definition env) definitions, aux env body) +*) | Ast.Uri (name, None) -> Ast.Uri (name, None) | Ast.Uri (name, Some substs) -> Ast.Uri (name, Some (aux_substs env substs))