diff options
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 21 |
1 files changed, 13 insertions, 8 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 28fd92659e..9777468374 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -22,6 +22,9 @@ open Constrextern open Ppconstr open Declarations +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + let emacs_str s = if !Flags.print_emacs then s else "" let delayed_emacs_cmd s = @@ -261,18 +264,21 @@ let pr_var_decl_skel pr_id env sigma (id,c,typ) = (pr_id id ++ hov 0 (pbody ++ ptyp)) let pr_var_decl env sigma d = - pr_var_decl_skel pr_id env sigma (Context.Named.Declaration.to_tuple d) + let d = match d with + | NamedDecl.LocalAssum (id,typ) -> id, None, typ + | NamedDecl.LocalDef (id,c,typ) -> id, Some c, typ + in + pr_var_decl_skel pr_id env sigma d let pr_var_list_decl env sigma (l,c,typ) = hov 0 (pr_var_decl_skel (fun ids -> prlist_with_sep pr_comma pr_id ids) env sigma (l,c,typ)) let pr_rel_decl env sigma decl = - let open Context.Rel.Declaration in - let na = get_name decl in - let typ = get_type decl in + let na = RelDecl.get_name decl in + let typ = RelDecl.get_type decl in let pbody = match decl with - | LocalAssum _ -> mt () - | LocalDef (_,c,_) -> + | RelDecl.LocalAssum _ -> mt () + | RelDecl.LocalDef (_,c,_) -> (* Force evaluation *) let pb = pr_lconstr_env env sigma c in let pb = if isCast c then surround pb else pb in @@ -417,8 +423,7 @@ let pr_evgl_sign sigma evi = | None -> [], [] | Some f -> List.filter2 (fun b c -> not b) f (evar_context evi) in - let open Context.Named.Declaration in - let ids = List.rev_map get_id l in + let ids = List.rev_map NamedDecl.get_id l in let warn = if List.is_empty ids then mt () else (str "(" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)") |