aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/context.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-08-17 16:14:35 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-08-17 16:14:50 +0200
commit3fd0b8ad700bd77aabdd3f3f33b13ba5e93d8bc8 (patch)
treef69f72d113b17ebb788ee5013b9d1c2ca3031a20 /kernel/context.mli
parent8e38b0e46f9628bcface1e5dad39c876f1f3f318 (diff)
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.
Diffstat (limited to 'kernel/context.mli')
-rw-r--r--kernel/context.mli2
1 files changed, 2 insertions, 0 deletions
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.