diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-06-29 14:30:33 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-29 14:30:33 +0200 |
| commit | 2ca003899ea4a24a470c32dc186b95ef3de3ca19 (patch) | |
| tree | e7444295b47223d16db6db5beafde4839a0cf926 /kernel/context.ml | |
| parent | acbc42ad1da48be53456c0d41ec2e60ae2d6e642 (diff) | |
| parent | 21ed95122a088cab6808200778719270d9cc9078 (diff) | |
Merge PR #7080: Swapping Context and Constr and defining declarations on constr in Constr
Diffstat (limited to 'kernel/context.ml')
| -rw-r--r-- | kernel/context.ml | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/kernel/context.ml b/kernel/context.ml index 5d4a10184..831dc850f 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -43,8 +43,6 @@ struct | LocalAssum of Name.t * 'types (** name, type *) | LocalDef of Name.t * 'constr * 'types (** name, value, type *) - type t = (Constr.constr, Constr.types) pt - (** Return the name bound by a given declaration. *) let get_name = function | LocalAssum (na,_) @@ -157,7 +155,6 @@ struct Inner-most declarations are at the beginning of the list. Outer-most declarations are at the end of the list. *) type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list - type t = Declaration.t list (** empty rel-context *) let empty = [] @@ -241,8 +238,6 @@ struct | LocalAssum of Id.t * 'types (** identifier, type *) | LocalDef of Id.t * 'constr * 'types (** identifier, value, type *) - type t = (Constr.constr, Constr.types) pt - (** Return the identifier bound by a given declaration. *) let get_id = function | LocalAssum (id,_) -> id @@ -370,7 +365,6 @@ struct Inner-most declarations are at the beginning of the list. Outer-most declarations are at the end of the list. *) type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list - type t = Declaration.t list (** empty named-context *) let empty = [] @@ -429,8 +423,6 @@ module Compacted = | LocalAssum of Id.t list * 'types | LocalDef of Id.t list * 'constr * 'types - type t = (Constr.constr, Constr.types) pt - let map_constr f = function | LocalAssum (ids, ty) as decl -> let ty' = f ty in @@ -454,7 +446,6 @@ module Compacted = end type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list - type t = Declaration.t list let fold f l ~init = List.fold_right f l init end |