diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/unification.ml | 2 | ||||
| -rw-r--r-- | pretyping/unification.mli | 2 |
2 files changed, 4 insertions, 0 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 9758aa43c4..510d5761b7 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -37,6 +37,8 @@ let _ = Goptions.declare_bool_option { Goptions.optwrite = (fun a -> keyed_unification:=a); } +let is_keyed_unification () = !keyed_unification + let debug_unification = ref (false) let _ = Goptions.declare_bool_option { Goptions.optsync = true; Goptions.optdepr = false; diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 119b1a7590..9246c10f90 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -42,6 +42,8 @@ val default_no_delta_unify_flags : unit -> unify_flags val elim_flags : unit -> unify_flags val elim_no_delta_flags : unit -> unify_flags +val is_keyed_unification : unit -> bool + (** The "unique" unification fonction *) val w_unify : env -> evar_map -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_map |