From 4841b790bbe517deefac11e8df1a7a1494d56bec Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 12 Jan 2016 17:02:09 +0100
Subject: 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.
---
 pretyping/unification.ml  | 2 ++
 pretyping/unification.mli | 2 ++
 2 files changed, 4 insertions(+)

(limited to 'pretyping')

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
-- 
cgit v1.2.3