CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" function

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)")