diff options
| author | Matej Kosik | 2016-08-26 13:23:37 +0200 |
|---|---|---|
| committer | Matej Kosik | 2016-08-26 13:23:37 +0200 |
| commit | ab9d2406975aba499d52f559e3303b82ce72d8ca (patch) | |
| tree | b1bfd60f6a8c897f96bacda48eb43a782a369c76 /printing/printer.ml | |
| parent | 69388fcd52b4a2aeefe843099c608d96defd1ce6 (diff) | |
CLEANUP: adding "Context.Compacted.Declaration.of_named_decl" function, which can be useful in general, and then simplifying "Printer.pr_named_decl" function
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 8 |
1 files changed, 1 insertions, 7 deletions
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 |