diff options
| author | Pierre-Marie Pédrot | 2018-03-27 16:16:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-26 13:50:10 +0200 |
| commit | de20a45db5d45154819f2ed4359effdbb8bf0292 (patch) | |
| tree | 4df0add753c3464868f3bc61350cdd9ff7dc445a /kernel/declarations.ml | |
| parent | 09c76adaff7adaada1c49479dfa9a4d0a4b416af (diff) | |
Turn the kernel reduction sharing flag into an argument passed in the cache.
We move the global declaration of that argument to the environment, and reuse
the Global module to handle this flag.
Note that the checker was not using this flag before this patch, and still
doesn't use it. This should probably be fixed in a later patch.
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 0811eb72fd..1d49550442 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -65,6 +65,7 @@ type typing_flags = { points are assumed to be total. *) check_universes : bool; (** If [false] universe constraints are not checked *) conv_oracle : Conv_oracle.oracle; (** Unfolding strategies for conversion *) + share_reduction : bool; (** Use by-need reduction algorithm *) } (* some contraints are in constant_constraints, some other may be in |