No hash consing across calls to the native compiler.

The induced side effects were incompatible with the undo machinery.

1 files changed, 4 insertions, 0 deletions

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