CLEANUP: adding "Context.Compacted.Declaration.of_named_decl" function, which can be useful in general, and then simplifying "Printer.pr_named_decl" function

3 files changed, 8 insertions, 7 deletions

diff --git a/kernel/context.ml b/kernel/context.ml
index f14bdc97b..ae0388003 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -429,6 +429,12 @@ module Compacted =
              let c' = f c in
              if c == c' && ty == ty' then decl else LocalDef (ids,c',ty')
 
+        let of_named_decl = function
+          | Named.Declaration.LocalAssum (id,t) ->
+              LocalAssum ([id],t)
+          | Named.Declaration.LocalDef (id,v,t) ->
+              LocalDef ([id],v,t)
+
         let to_named_context = function
           | LocalAssum (ids, t) ->
              List.map (fun id -> Named.Declaration.LocalAssum (id,t)) ids
diff --git a/kernel/context.mli b/kernel/context.mli
index 091d701a2..955e214cb 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -260,6 +260,7 @@ sig
       | LocalDef of Id.t list * Constr.t * Constr.t
 
     val map_constr : (Constr.t -> Constr.t) -> t -> t
+    val of_named_decl : Named.Declaration.t -> t
     val to_named_context : t -> Named.t
   end
 
diff --git a/printing/printer.ml b/printing/printer.ml
index 77423d32a..a6c7c5ca1 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -268,13 +268,7 @@ let pr_compacted_decl env sigma decl =
   hov 0 (pids ++ pbody ++ ptyp)
 
 let pr_named_decl env sigma decl =
-  let decl = match decl with
-    | NamedDecl.LocalAssum (id, t) ->
-       CompactedDecl.LocalAssum ([id], t)
-    | NamedDecl.LocalDef (id,c,t) ->
-       CompactedDecl.LocalDef ([id],c,t)
-  in
-  pr_compacted_decl env sigma decl
+  decl |> CompactedDecl.of_named_decl |> pr_compacted_decl env sigma
 
 let pr_rel_decl env sigma decl =
   let na = RelDecl.get_name decl in