From 8e38b0e46f9628bcface1e5dad39c876f1f3f318 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Thu, 11 Aug 2016 14:37:45 +0200 Subject: Adding "Context.Named.Declaraton.of_rel" function --- kernel/context.mli | 3 +++ 1 file changed, 3 insertions(+) (limited to 'kernel/context.mli') 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. -- cgit v1.2.3