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 /kernel/context.ml | |
| 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.
Diffstat (limited to 'kernel/context.ml')
| -rw-r--r-- | kernel/context.ml | 5 |
1 files changed, 5 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. |