diff options
| author | Pierre-Marie Pédrot | 2018-07-25 15:56:49 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-25 15:56:49 +0200 |
| commit | 523de4f878293cf1d582bd70300b34d497e705b3 (patch) | |
| tree | 5037ac2e2fd60003d582d800466657df624b848f /kernel/declarations.ml | |
| parent | 9b6ce4f1848c546d0d361aa1089fa2907ca4c9ad (diff) | |
| parent | cb219011534a8de24a01ddb007799133cdd2cb0e (diff) | |
Merge PR #7889: Cleanup reduction effects: they only work on constants.
Diffstat (limited to 'kernel/declarations.ml')
0 files changed, 0 insertions, 0 deletions