diff options
| -rw-r--r-- | src/Util/Strings/String.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Util/Strings/String.v b/src/Util/Strings/String.v index 3661d816f..adea76d48 100644 --- a/src/Util/Strings/String.v +++ b/src/Util/Strings/String.v @@ -283,4 +283,7 @@ Proof. { Abort. +Definition replace (from to s : string) : string + := concat to (split from s). + Notation NewLine := (String Ascii.NewLine ""). |