From 3fd0b8ad700bd77aabdd3f3f33b13ba5e93d8bc8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 17 Aug 2016 16:14:35 +0200 Subject: Revert "CLEANUP: removing the definition of the "Context.Rel.Declaration.to_tuple" function" This reverts commit 4b24bb7d3b770592015c264001b9aed9fe95c200. While the of_tuple function is clearly dubious and mostly used for compatiblity reasons, and thus had to be removed, I think that the to_tuple function is still useful as it allows to access each component of the declaration piecewise. Without it, some codes tend to get cluttered with useless projections here and there. --- kernel/context.mli | 2 ++ 1 file changed, 2 insertions(+) (limited to 'kernel/context.mli') diff --git a/kernel/context.mli b/kernel/context.mli index 27d0f2c1b..b8a7bf6a3 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -80,6 +80,8 @@ sig (** Reduce all terms in a given declaration to a single value. *) val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a + + val to_tuple : t -> Name.t * Constr.t option * Constr.t end (** Rel-context is represented as a list of declarations. -- cgit v1.2.3