Add str.unit to LFSC signature (#8862)

Fixes buildbot failure.

diff --git a/proofs/lfsc/signatures/theory_def.plf b/proofs/lfsc/signatures/theory_def.plf
index df0abe39594164a8575126b2cf0bb2fae5f99ebe..04ac320aeb7843f479bda0bd22c2c9c3d3788f18 100644 (file)
--- a/proofs/lfsc/signatures/theory_def.plf
+++ b/proofs/lfsc/signatures/theory_def.plf
@@ -170,6 +170,8 @@
 (define str.suffixof (# x term (# y term (apply (apply f_str.suffixof x) y))))
 (declare f_str.rev term)
 (define str.rev (# x term (apply f_str.rev x)))
+(declare f_str.unit term)
+(define str.unit (# x term (apply f_str.unit x)))
 (declare f_str.update term)
 (define str.update (# x term (# y term (# z term (apply (apply (apply f_str.update x) y) z)))))
 (declare f_str.to_lower term)