diff options
| author | Emilio Jesus Gallego Arias | 2019-05-01 08:28:57 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-05-01 18:49:02 +0200 |
| commit | ba5ea9fb6aaa3faace0960adca4d41fc74cb2ac7 (patch) | |
| tree | ab14d96954dce28fd46a32960c446f068ccae9f0 /dev/dynlink.ml | |
| parent | 213b5419136e4639f345e171c086b154c14aa62c (diff) | |
[comDefinition] Use prepare function from DeclareDef.
We also update the plugin tutorial.
This was already tried [in the same exact way] in #8811, however the
bench time was not convincing then, but now things seem a bit better,
likely due to the removal of some extra normalization somewhere.
Some more changes from #8811 are still pending.
Diffstat (limited to 'dev/dynlink.ml')
0 files changed, 0 insertions, 0 deletions