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.ml  | 6 ++++++
 kernel/context.mli | 3 +++
 2 files changed, 9 insertions(+)

(limited to 'kernel')

diff --git a/kernel/context.ml b/kernel/context.ml
index 2f4997055d..ca084b6820 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -340,6 +340,12 @@ struct
     let of_tuple = function
       | id, None, ty -> LocalAssum (id, ty)
       | id, Some v, ty -> LocalDef (id, v, ty)
+
+    let of_rel f = function
+      | Rel.Declaration.LocalAssum (na,t) ->
+          LocalAssum (f na, t)
+      | Rel.Declaration.LocalDef (na,v,t) ->
+          LocalDef (f na, v, t)
   end
 
   (** Named-context is represented as a list of declarations.
diff --git a/kernel/context.mli b/kernel/context.mli
index 55ea8921be..27d0f2c1bd 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