diff options
| author | Hugo Herbelin | 2020-02-08 12:35:27 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-08 12:35:27 +0100 |
| commit | 3e460f77c1777ce1a8d393f2335fd7f4b4fe924f (patch) | |
| tree | da7b940e3f98901c063101cf38eff0550ec48bb9 /kernel/context.mli | |
| parent | c2f0b3c6c6942d8821ce05759b6940bd77435602 (diff) | |
Fixing wrong comments in context.ml.
Diffstat (limited to 'kernel/context.mli')
| -rw-r--r-- | kernel/context.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/context.mli b/kernel/context.mli index 8f233613da..04aa039a01 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -129,7 +129,7 @@ sig (** Return a new rel-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 context. *) + (** Return the number of {e local declarations} in a given rel-context. *) val length : ('c, 't) pt -> int (** Check whether given two rel-contexts are equal. *) |