From 6f6eaa858a2a4268b8c6a63a284e9d07941b511f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 24 Oct 2014 00:10:38 +0200
Subject: No hash consing across calls to the native compiler.

The induced side effects were incompatible with the undo machinery.
---
 kernel/nativecode.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'kernel/nativecode.ml')

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index c8a4fa897c..4263b3b508 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1949,6 +1949,8 @@ let mk_internal_let s code =
 
 (* ML Code for conversion function *)
 let mk_conv_code env sigma prefix t1 t2 =
+  clear_symb_tbl ();
+  clear_global_tbl ();
   let gl, (mind_updates, const_updates) =
     let init = ([], empty_updates) in
     compile_deps env sigma prefix ~interactive:true init t1
@@ -1974,6 +1976,8 @@ let mk_conv_code env sigma prefix t1 t2 =
   header::gl, (mind_updates, const_updates)
 
 let mk_norm_code env sigma prefix t =
+  clear_symb_tbl ();
+  clear_global_tbl ();
   let gl, (mind_updates, const_updates) =
     let init = ([], empty_updates) in
     compile_deps env sigma prefix ~interactive:true init t
-- 
cgit v1.2.3