diff options
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. |