diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-01-12 17:02:09 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-01-12 17:28:04 +0100 |
| commit | 4841b790bbe517deefac11e8df1a7a1494d56bec (patch) | |
| tree | 66f0618b7e63dfd4d6970faf19ebe441ba1e5fb9 /pretyping/unification.mli | |
| parent | 94b3068c688b289ec26005d13251fc1c3dae6998 (diff) | |
Fix essential bug in new Keyed Unification mode reported by R. Krebbers.
[rewrite] was calling find_suterm using the wrong unification flags, not
allowing full delta in unification of terms with the right keys as desired.
Diffstat (limited to 'pretyping/unification.mli')
| -rw-r--r-- | pretyping/unification.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 119b1a759..9246c10f9 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 |