From 7e7919950d340a08e62a3a9dc8b6f72b56cefa2b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 5 Nov 2015 16:32:59 -0800
Subject: [PATCH] fix(library/type_context): compilation warning

---
 src/library/type_context.h | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/library/type_context.h b/src/library/type_context.h
index 084c0e9ee..1ac729925 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -22,6 +22,7 @@ class tmp_local_generator {
     name mk_fresh_name();
 public:
     tmp_local_generator();
+    virtual ~tmp_local_generator() {}
 
     /** \brief Create a temporary local constant */
     virtual expr mk_tmp_local(expr const & type, binder_info const & bi);