From 79c1aed726d9532125305af52ecbb010847a8a2c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 27 Sep 2021 20:43:50 +0200 Subject: fix clightgen --- exportclight/ExportClight.ml | 3 +++ 1 file changed, 3 insertions(+) (limited to 'exportclight') 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) -> -- cgit