diff options
| author | Théo Zimmermann | 2018-09-12 22:08:23 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-12 22:08:23 +0200 |
| commit | 55be260b9abb8e2b3382f7b44b35e46b241a1d57 (patch) | |
| tree | d90d82639052c86283675c157638730d6eab7516 /kernel | |
| parent | 26936e66c7c16f72fd1a7978505c95af9899ddc0 (diff) | |
Fix mli-doc following #7109.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/constr.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/constr.mli b/kernel/constr.mli index 57784581ee..9cc044316b 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -382,7 +382,7 @@ type named_context = named_declaration list type compacted_context = compacted_declaration list (** {6 Functionals working on expressions canonically abstracted over - a local context (possibly with let-ins) *) + a local context (possibly with let-ins)} *) (** [map_under_context f l c] maps [f] on the immediate subterms of a term abstracted over a context of length [n] (local definitions |