diff options
Diffstat (limited to 'lib/pp_diff.mli')
| -rw-r--r-- | lib/pp_diff.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/pp_diff.mli b/lib/pp_diff.mli index 03468271d2..24f2eace93 100644 --- a/lib/pp_diff.mli +++ b/lib/pp_diff.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -88,7 +88,7 @@ Ppcmd_strings will be split into multiple Ppcmd_strings if a diff starts or ends in the middle of the string. Whitespace just before or just after a diff will not be part of the highlight. -Prexisting tags in pp may contain only a single Ppcmd_string. Those tags will be +Preexisting tags in pp may contain only a single Ppcmd_string. Those tags will be placed inside the diff tags to ensure proper nesting of tags within spans of "start.diff.*" ... "end.diff.*". |