From 8eae572c0bbc0a3f597f43a00c0c84875bcf2286 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 25 Feb 2014 11:05:06 +0100
Subject: Library: when compiling multiple files, reset the opaque tables

That was a bug. coqc a b was generating (for b) an opaque table containing
also the proofs of a.
---
 library/library.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'library')

diff --git a/library/library.ml b/library/library.ml
index ccf2821756..64c2c2ad59 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -422,6 +422,13 @@ module OpaqueTables = struct
    Array.sub !local_discharge_table 0 !local_index,
    FMap.bindings !f2t
 
+ let reset () =
+   local_discharge_table := Array.make 100 a_discharge;
+   local_univ_table := Array.make 100 a_univ;
+   local_opaque_table := Array.make 100 a_constr;
+   f2t := FMap.empty;
+   local_index := 0
+
 end
 
 let () =
@@ -659,6 +666,7 @@ let start_library f =
   let id = Id.of_string (Filename.basename f) in
   check_coq_overwriting ldir0 id;
   let ldir = add_dirpath_suffix ldir0 id in
+  OpaqueTables.reset ();
   Opaqueproof.set_indirect_creator OpaqueTables.store;
   Declaremods.start_library ldir;
   ldir,longf
-- 
cgit v1.2.3