diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-03-22 00:49:36 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-03-22 00:49:36 +0100 |
commit | 051ef20a9f9c496fc6a5143de97450ccf7786c5b (patch) | |
tree | b298a34e49450cbff00ac4341d7d64cbac8e537a /test-suite/output/RealSyntax.v | |
parent | 151286ec0c0887d212e7e85205352de4ddbf4bf2 (diff) | |
parent | addc1304de75800fa9301e97d3ae78539f511959 (diff) |
Merge PR#478: Small optimization on handling of library state.
Diffstat (limited to 'test-suite/output/RealSyntax.v')
0 files changed, 0 insertions, 0 deletions