diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-02-25 11:05:06 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-02-26 14:53:08 +0100 |
| commit | 8eae572c0bbc0a3f597f43a00c0c84875bcf2286 (patch) | |
| tree | a06a2b886f5d2b229765bb474df090ec78675f05 /library/library.ml | |
| parent | 02ca1e0bc62f58a5f5d321c42452509b9ec1f198 (diff) | |
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.
Diffstat (limited to 'library/library.ml')
| -rw-r--r-- | library/library.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/library/library.ml b/library/library.ml index ccf282175..64c2c2ad5 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 |