diff options
| -rw-r--r-- | kernel/context.ml | 6 | ||||
| -rw-r--r-- | kernel/context.mli | 1 | ||||
| -rw-r--r-- | printing/printer.ml | 8 |
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 |