summaryrefslogtreecommitdiff
path: root/src/rewriter.mli
diff options
context:
space:
mode:
authorJon French2018-06-11 16:38:53 +0100
committerJon French2018-06-11 16:38:53 +0100
commit6b70f78c3c9477d4c5f417ed0a5d96abc19c9fb0 (patch)
tree5d8bdfd982c5c0efde9c7eac021f6341af124e7f /src/rewriter.mli
parent0cc7d50e08b36d036771493920bb2e20251def64 (diff)
parent22aff19aeea53719004cca2b5c6b25d0a7ed0835 (diff)
Merge branch 'mappings' into sail2
Diffstat (limited to 'src/rewriter.mli')
-rw-r--r--src/rewriter.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 6e9f08c2..edc93e5d 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -95,6 +95,7 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
; p_tup : 'pat list -> 'pat_aux
; p_list : 'pat list -> 'pat_aux
; p_cons : 'pat * 'pat -> 'pat_aux
+ ; p_string_append : 'pat list -> 'pat_aux
; p_aux : 'pat_aux * 'a annot -> 'pat
; fP_aux : 'fpat_aux * 'a annot -> 'fpat
; fP_Fpat : id * 'pat -> 'fpat_aux