diff options
| author | Matthieu Sozeau | 2016-01-12 17:02:09 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-01-12 17:28:04 +0100 |
| commit | 4841b790bbe517deefac11e8df1a7a1494d56bec (patch) | |
| tree | 66f0618b7e63dfd4d6970faf19ebe441ba1e5fb9 /pretyping | |
| 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')
| -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 |