aboutsummaryrefslogtreecommitdiffstats
path: root/export/ExportCsyntax.ml
diff options
context:
space:
mode:
authorDavid Monniaux <David.Monniaux@univ-grenoble-alpes.fr>2021-09-27 20:48:57 +0200
committerDavid Monniaux <David.Monniaux@univ-grenoble-alpes.fr>2021-09-27 20:48:57 +0200
commit95836bb256258951d10d1c5b59db6352ce241a12 (patch)
tree4b9a058f11db91faa4a45e40179200963fe8dca6 /export/ExportCsyntax.ml
parent6b897598b16912661bc681f8e60428de6ad2018a (diff)
parent79c1aed726d9532125305af52ecbb010847a8a2c (diff)
downloadcompcert-kvx-95836bb256258951d10d1c5b59db6352ce241a12.tar.gz
compcert-kvx-95836bb256258951d10d1c5b59db6352ce241a12.zip
Merge remote-tracking branch 'origin/kvx-work' into towards_3.10
Diffstat (limited to 'export/ExportCsyntax.ml')
-rw-r--r--export/ExportCsyntax.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/export/ExportCsyntax.ml b/export/ExportCsyntax.ml
index 1d91cba5..25d8526b 100644
--- a/export/ExportCsyntax.ml
+++ b/export/ExportCsyntax.ml
@@ -54,6 +54,7 @@ let name_binop = function
| Ogt -> "Ogt"
| Ole -> "Ole"
| Oge -> "Oge"
+ | Oexpect -> "Oexpect"
let name_incr_or_decr = function
| Incr -> "Incr"