diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2016-08-26 13:23:37 +0200 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-08-26 13:23:37 +0200 |
| commit | ab9d2406975aba499d52f559e3303b82ce72d8ca (patch) | |
| tree | b1bfd60f6a8c897f96bacda48eb43a782a369c76 /kernel/context.mli | |
| 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 'kernel/context.mli')
| -rw-r--r-- | kernel/context.mli | 1 |
1 files changed, 1 insertions, 0 deletions
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 |