diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-17 16:14:35 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-17 16:14:50 +0200 |
commit | 3fd0b8ad700bd77aabdd3f3f33b13ba5e93d8bc8 (patch) | |
tree | f69f72d113b17ebb788ee5013b9d1c2ca3031a20 | |
parent | 8e38b0e46f9628bcface1e5dad39c876f1f3f318 (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.
-rw-r--r-- | kernel/context.ml | 5 | ||||
-rw-r--r-- | kernel/context.mli | 2 |
2 files changed, 7 insertions, 0 deletions
diff --git a/kernel/context.ml b/kernel/context.ml index ca084b682..269bf2143 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -142,6 +142,11 @@ struct match decl with | LocalAssum (n,ty) -> f ty acc | LocalDef (n,v,ty) -> f ty (f v acc) + + let to_tuple = function + | LocalAssum (na, ty) -> na, None, ty + | LocalDef (na, v, ty) -> na, Some v, ty + end (** Rel-context is represented as a list of declarations. 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. |