aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/ProgramWf.v
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2015-12-15 18:56:08 +0100
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2015-12-15 19:04:44 +0100
commit0a89d4805a29628c82b994958362dc9d92709020 (patch)
treed4857b563a5f063a7a6a9a3f47ea15f84a823ba8 /test-suite/success/ProgramWf.v
parent34ea06f2f31cebf00bc7620fac34d963afe6a1dc (diff)
Extraction: more cautious use of intermediate result caching (fix #3923)
During an extraction, a few tables are maintained to cache intermediate results. Due to modules, the kernel_name index for these caching tables aren't enough. For instance, in bug #3923, a constant is first transparent (from inside the module) then opaque (when seen from the signature). The previous protections were actually obsolete (tests via visible_con), we now checks that the constant_body is still the same.
Diffstat (limited to 'test-suite/success/ProgramWf.v')
0 files changed, 0 insertions, 0 deletions