From ab9d2406975aba499d52f559e3303b82ce72d8ca Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Fri, 26 Aug 2016 13:23:37 +0200
Subject: CLEANUP: adding "Context.Compacted.Declaration.of_named_decl"
 function, which can be useful in general, and then simplifying
 "Printer.pr_named_decl" function

---
 printing/printer.ml | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

(limited to 'printing')

diff --git a/printing/printer.ml b/printing/printer.ml
index 77423d32a7..a6c7c5ca1f 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
-- 
cgit v1.2.3