diff options
| author |  Matej Kosik <matej.kosik@inria.fr> | 2017-02-09 18:33:56 +0100 |
|---|---|---|
| committer | Matej Košík <matej.kosik@inria.fr> | 2017-04-20 13:11:50 +0200 |
| commit | 4fc8616852438e80b10e0247550cc8968d76e9d7 (patch) | |
| tree | 17e9c8f43a1a082fa81cc125fbdaf774be4e70ec /kernel/context.mli | |
| parent | bbec61be495db3de93fc17830405b6d80a271496 (diff) | |
correcting comments in the "Context" module
Diffstat (limited to 'kernel/context.mli')
| -rw-r--r-- | kernel/context.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/kernel/context.mli b/kernel/context.mli index 0c666a25d..24e69ebd6 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -214,7 +214,7 @@ sig val to_rel_decl : ('c, 't) pt -> ('c, 't) Rel.Declaration.pt end - (** Rel-context is represented as a list of declarations. + (** Named-context is represented as a list of declarations. 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 @@ -223,7 +223,7 @@ sig (** empty named-context *) val empty : ('c, 't) pt - (** Return a new rel-context enriched by with a given inner-most declaration. *) + (** Return a new named-context enriched by with a given inner-most declaration. *) val add : ('c, 't) Declaration.pt -> ('c, 't) pt -> ('c, 't) pt (** Return the number of {e local declarations} in a given named-context. *) @@ -233,7 +233,7 @@ sig @raise Not_found if the designated identifier is not bound in a given named-context. *) val lookup : Id.t -> ('c, 't) pt -> ('c, 't) Declaration.pt - (** Check whether given two rel-contexts are equal. *) + (** Check whether given two named-contexts are equal. *) val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool (** Map all terms in a given named-context. *) @@ -253,8 +253,8 @@ sig (** Return the set of all identifiers bound in a given named-context. *) val to_vars : ('c, 't) pt -> Id.Set.t - (** [instance_from_named_context Ω] builds an instance [args] such - that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local + (** [to_instance Ω] builds an instance [args] such + that [Ω ⊢ args:Ω] where [Ω] is a named-context and with the local definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it gives [Var id1, Var id3]. All [idj] are supposed distinct. *) val to_instance : (Id.t -> 'r) -> ('c, 't) pt -> 'r list |