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.mli | |
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.mli')
-rw-r--r-- | kernel/context.mli | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/kernel/context.mli b/kernel/context.mli index c97db4348..957ac4b3d 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -35,8 +35,6 @@ sig | 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. *) val get_name : ('c, 't) pt -> Name.t @@ -93,7 +91,6 @@ sig 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 *) val empty : ('c, 't) pt @@ -153,8 +150,6 @@ sig | 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. *) val get_id : ('c, 't) pt -> Id.t @@ -220,7 +215,6 @@ sig 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 *) val empty : ('c, 't) pt @@ -270,15 +264,12 @@ sig | LocalAssum of Id.t list * 'types | LocalDef of Id.t list * 'constr * 'types - type t = (Constr.constr, Constr.types) pt - val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt val of_named_decl : ('c, 't) Named.Declaration.pt -> ('c, 't) pt val to_named_context : ('c, 't) pt -> ('c, 't) Named.pt end type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list - type t = Declaration.t list val fold : (('c, 't) Declaration.pt -> 'a -> 'a) -> ('c, 't) pt -> init:'a -> 'a end |