diff options
Diffstat (limited to 'pretyping/unification.mli')
| -rw-r--r-- | pretyping/unification.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/unification.mli b/pretyping/unification.mli index aa0267698..44b1c3889 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -18,6 +18,7 @@ type unify_flags = { resolve_evars : bool; use_evars_pattern_unification : bool; frozen_evars : ExistentialSet.t; + restrict_conv_on_strict_subterms : bool; modulo_betaiota : bool; modulo_eta : bool; allow_K_in_toplevel_higher_order_unification : bool |