diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-09-27 20:48:57 +0200 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-09-27 20:48:57 +0200 |
| commit | 95836bb256258951d10d1c5b59db6352ce241a12 (patch) | |
| tree | 4b9a058f11db91faa4a45e40179200963fe8dca6 /export | |
| parent | 6b897598b16912661bc681f8e60428de6ad2018a (diff) | |
| parent | 79c1aed726d9532125305af52ecbb010847a8a2c (diff) | |
| download | compcert-kvx-95836bb256258951d10d1c5b59db6352ce241a12.tar.gz compcert-kvx-95836bb256258951d10d1c5b59db6352ce241a12.zip | |
Merge remote-tracking branch 'origin/kvx-work' into towards_3.10
Diffstat (limited to 'export')
| -rw-r--r-- | export/ExportBase.ml | 1 | ||||
| -rw-r--r-- | export/ExportClight.ml | 1 | ||||
| -rw-r--r-- | export/ExportCsyntax.ml | 1 |
3 files changed, 3 insertions, 0 deletions
diff --git a/export/ExportBase.ml b/export/ExportBase.ml index 4b93d8a9..b6388768 100644 --- a/export/ExportBase.ml +++ b/export/ExportBase.ml @@ -219,6 +219,7 @@ let external_function p = function coqstring text signatur sg (print_list coqstring) clob + | EF_profiling(_ ,_) -> failwith "EF_profiling in export" (* Variables *) diff --git a/export/ExportClight.ml b/export/ExportClight.ml index e3b00986..959c4f5c 100644 --- a/export/ExportClight.ml +++ b/export/ExportClight.ml @@ -50,6 +50,7 @@ let name_binop = function | Ogt -> "Ogt" | Ole -> "Ole" | Oge -> "Oge" + | Oexpect -> "Oexpect" let rec expr p = function | Evar(id, t) -> 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" |