diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-16 00:05:03 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-26 15:12:10 +0200 |
| commit | ce830b204ad52f8b3655d2cb4672662120d83101 (patch) | |
| tree | 988e160ecf888787c6d005b08db0cdfd62935460 /vernac/obligations.ml | |
| parent | 3fcf0930874d7200f2503ac7084b1d6669d59540 (diff) | |
Further simplication: do not recreate entries for side-effects.
This is actually useless, the code does not depend on the value of the
entry for side-effects.
Diffstat (limited to 'vernac/obligations.ml')
0 files changed, 0 insertions, 0 deletions