diff options
| author | Matej Kosik | 2016-02-09 18:07:53 +0100 |
|---|---|---|
| committer | Matej Kosik | 2016-02-09 18:07:53 +0100 |
| commit | 5dfb5d5e48c86dabd17ee2167c6fd5304c788474 (patch) | |
| tree | a3f39dd3b5055262149329944f2957c9cce247f6 /kernel/context.mli | |
| parent | 34ef02fac1110673ae74c41c185c228ff7876de2 (diff) | |
REFORMATTING: kernel/context.ml{,i}
Diffstat (limited to 'kernel/context.mli')
| -rw-r--r-- | kernel/context.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/context.mli b/kernel/context.mli index a69754cc29..b5f3904d22 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -29,8 +29,8 @@ sig module Declaration : sig (* local declaration *) - type t = LocalAssum of Name.t * Constr.t (* local assumption *) - | LocalDef of Name.t * Constr.t * Constr.t (* local definition *) + type t = LocalAssum of Name.t * Constr.t (** name, type *) + | LocalDef of Name.t * Constr.t * Constr.t (** name, value, type *) (** Return the name bound by a given declaration. *) val get_name : t -> Name.t @@ -143,8 +143,8 @@ sig (** Representation of {e local declarations}. *) module Declaration : sig - type t = LocalAssum of Id.t * Constr.t - | LocalDef of Id.t * Constr.t * Constr.t + type t = LocalAssum of Id.t * Constr.t (** identifier, type *) + | LocalDef of Id.t * Constr.t * Constr.t (** identifier, value, type *) (** Return the identifier bound by a given declaration. *) val get_id : t -> Id.t |