diff options
| author | Maxime Dénès | 2018-10-31 16:12:26 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-10-31 16:16:41 +0100 |
| commit | c367e7cd962089d2932b986e5764b8e3844ad4b0 (patch) | |
| tree | 55f75f93217a8f41c972b6f9514b62bdad1f1b30 /kernel/declarations.ml | |
| parent | c3ea3cd8a2bd29fc0129e34af4a1689bbf7519a5 (diff) | |
Use standard combinator for Global.set_strategy
Diffstat (limited to 'kernel/declarations.ml')
0 files changed, 0 insertions, 0 deletions