diff options
| author |  Matej Kosik <matej.kosik@inria.fr> | 2016-08-15 14:14:14 +0200 |
|---|---|---|
| committer |  Matej Kosik <m4tej.kosik@gmail.com> | 2016-08-25 10:52:44 +0200 |
| commit | 1297523bffdc3a9fe3e447acc6837be835e86d06 (patch) | |
| tree | 04b0db664081d14add21fe3a9934d609d8b749f0 /kernel/context.mli | |
| parent | 3e6bc0e8d09e3eb913b366b4f5db280154b94018 (diff) | |
CLEANUP: changing the definition of the "Context.NamedList.Declaration" type
Diffstat (limited to 'kernel/context.mli')
| -rw-r--r-- | kernel/context.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/kernel/context.mli b/kernel/context.mli index c5da51381..72fbfb540 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -255,8 +255,12 @@ module NamedList : sig module Declaration : sig - type t = Id.t list * Constr.t option * Constr.t + type t = + | LocalAssum of Id.t list * Constr.t + | LocalDef of Id.t list * Constr.t * Constr.t + val map_constr : (Constr.t -> Constr.t) -> t -> t + val to_named_context : t -> Named.t end type t = Declaration.t list |