diff options
| author | Maxime Dénès | 2018-09-03 12:36:45 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-03 12:36:45 +0200 |
| commit | 3bc0c82700a805e889198b810cc0148f6479cbe1 (patch) | |
| tree | eac2cce0546a79cb5786e0570c0c55b9b4438e4b /kernel/declareops.ml | |
| parent | 7456164386a87df83763109e12fa8aaa71a96104 (diff) | |
| parent | 14a1786158ec093faa172a5b95a93b06ad43b7af (diff) | |
Merge PR #7085: Turn the kernel reduction sharing flag into an argument passed in the cache
Diffstat (limited to 'kernel/declareops.ml')
| -rw-r--r-- | kernel/declareops.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index bbe4bc0dcb..b0d8410873 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -21,6 +21,7 @@ let safe_flags oracle = { check_guarded = true; check_universes = true; conv_oracle = oracle; + share_reduction = true; } (** {6 Arities } *) |