diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-09-27 20:43:50 +0200 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-09-27 20:43:50 +0200 |
| commit | 79c1aed726d9532125305af52ecbb010847a8a2c (patch) | |
| tree | a243040d7e6a28d8ebbfecf7843e2aee0061346c /exportclight | |
| parent | 9d3103177c6838541f3a21caa6716381a50dc817 (diff) | |
| download | compcert-kvx-79c1aed726d9532125305af52ecbb010847a8a2c.tar.gz compcert-kvx-79c1aed726d9532125305af52ecbb010847a8a2c.zip | |
fix clightgen
Diffstat (limited to 'exportclight')
| -rw-r--r-- | exportclight/ExportClight.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index 474a1bd8..9937e5e7 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -287,6 +287,8 @@ let external_function p = function coqstring text signatur sg (print_list coqstring) clob + | EF_profiling(id, kind) -> + fprintf p "EF_profiling" (* should not happen *) (* Expressions *) @@ -313,6 +315,7 @@ let name_binop = function | Ogt -> "Ogt" | Ole -> "Ole" | Oge -> "Oge" + | Oexpect -> "Oexpect" let rec expr p = function | Evar(id, t) -> |