From: Claudio Sacerdoti Coen Date: Fri, 13 Oct 2006 16:59:04 +0000 (+0000) Subject: Content level representation of LetRec changed. X-Git-Tag: 0.4.95@7852~890 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6935786198ad90e697125917839f7adfe5b04368;p=helm.git Content level representation of LetRec changed. --- diff --git a/components/content_pres/termContentPres.ml b/components/content_pres/termContentPres.ml index 96a15c01e..e925db0aa 100644 --- a/components/content_pres/termContentPres.ml +++ b/components/content_pres/termContentPres.ml @@ -206,23 +206,36 @@ let pp_ast0 t k = let rec_op = match rec_kind with `Inductive -> "rec" | `CoInductive -> "corec" in - let mk_fun (var, body, _) = aux_var var, k body in + let mk_fun (args, (name,ty), body, _) = + List.map aux_var args ,k name, HExtlib.map_option k ty, k body in let mk_funs = List.map mk_fun in let fst_fun, tl_funs = match mk_funs funs with hd :: tl -> hd, tl | [] -> assert false in let fst_row = - let (name, body) = fst_fun in - hvbox false true [ - keyword "let"; keyword rec_op; name; builtin_symbol "\\def"; break; - top_pos body ] + let (params, name, ty, body) = fst_fun in + hvbox false true ([ + keyword "let"; + keyword rec_op; + name] @ + params @ + (match ty with None -> [] | Some ty -> [builtin_symbol ":"; ty]) @ + [ builtin_symbol "\\def"; + break; + top_pos body ]) in let tl_rows = List.map - (fun (name, body) -> + (fun (params, name, ty, body) -> [ break; - hvbox false true [ - keyword "and"; name; builtin_symbol "\\def"; break; body ] ]) + hvbox false true ([ + keyword "and"; + name] @ + params @ + (match ty with + None -> [] + | Some ty -> [builtin_symbol ":"; ty]) @ + [ builtin_symbol "\\def"; break; body ])]) tl_funs in add_level_info Ast.let_in_prec Ast.let_in_assoc @@ -555,8 +568,8 @@ let instantiate_level2 env term = (aux_pattern env pattern, aux env term) and aux_pattern env (head, hrefs, vars) = (head, hrefs, List.map (aux_capture_var env) vars) - and aux_definition env (var, term, i) = - (aux_capture_var env var, aux env term, i) + and aux_definition env (params, var, term, i) = + (List.map (aux_capture_var env) params, aux_capture_var env var, aux env term, i) and aux_substs env substs = List.map (fun (name, term) -> (name, aux env term)) substs and aux_meta_substs env meta_substs = List.map (aux_opt env) meta_substs