aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/context.mli
diff options
context:
space:
mode:
authorGravatar Matej Kosik <m4tej.kosik@gmail.com>2016-08-11 14:37:45 +0200
committerGravatar Matej Kosik <m4tej.kosik@gmail.com>2016-08-11 15:01:31 +0200
commit8e38b0e46f9628bcface1e5dad39c876f1f3f318 (patch)
treec53f745aa1d4a1eaeec081baaec649cd815d2dfa /kernel/context.mli
parentbf7515a299d894762e10cf0f116e156073071879 (diff)
Adding "Context.Named.Declaraton.of_rel" function
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.