diff options
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 |