diff options
Diffstat (limited to 'pretyping/unification.mli')
| -rw-r--r-- | pretyping/unification.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 1b8f9ccd8..8cfa20948 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -17,11 +17,12 @@ open Evd type unify_flags = { modulo_conv_on_closed_terms : Names.transparent_state option; use_metas_eagerly : bool; + use_types : bool; modulo_delta : Names.transparent_state; } val default_unify_flags : unify_flags -val default_no_delta_unify_flags : unify_flags +val simple_apply_unify_flags : unify_flags (* The "unique" unification fonction *) val w_unify : |