aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/context.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/context.mli')
-rw-r--r--kernel/context.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/context.mli b/kernel/context.mli
index 55ea8921b..27d0f2c1b 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -194,6 +194,9 @@ sig
val to_tuple : t -> Id.t * Constr.t option * Constr.t
val of_tuple : Id.t * Constr.t option * Constr.t -> t
+
+ (** Convert [Rel.Declaration.t] value to the corresponding [Named.Declaration.t] value. *)
+ val of_rel : (Name.t -> Id.t) -> Rel.Declaration.t -> t
end
(** Rel-context is represented as a list of declarations.