From 22ced4748484bbc0e930efd74f7d162fe561fe32 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 15 Mar 2019 20:54:52 +0000
Subject: Don't constant-fold undefined_X functions in monomorphisation

These should be preserved for prover backends.
---
 src/initial_check.mli | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'src/initial_check.mli')

diff --git a/src/initial_check.mli b/src/initial_check.mli
index b41b1818..59c8f0b6 100644
--- a/src/initial_check.mli
+++ b/src/initial_check.mli
@@ -87,6 +87,11 @@ val opt_enum_casts : bool ref
    all the loaded files. *)
 val have_undefined_builtins : bool ref
 
+(** Val specs of undefined functions for builtin types that get added to
+    the AST if opt_undefined_gen is set (minus those functions that already
+    exist in the AST). *)
+val undefined_builtin_val_specs : unit def list
+
 (** {2 Desugar and process AST } *)
 
 (** If the generate flag is false, then we won't generate any
-- 
cgit v1.2.3