4 files changed, 2 insertions, 4 deletions
diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
index f4e2ac8..72161e7 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
@@ -1093,7 +1093,7 @@ let interp_refine ist gl rc =
   let kind = OfType (pf_concl gl) in
   let flags = {
     use_typeclasses = true;
-    use_unif_heuristics = true;
+    solve_unification_constraints = true;
     use_hook = None;
     fail_evar = false;
     expand_evars = true }
diff --git a/mathcomp/ssreflect/plugin/v8.6/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.6/ssreflect.ml4
index 1e122ea..6aaa79b 100644
--- a/mathcomp/ssreflect/plugin/v8.6/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/v8.6/ssreflect.ml4
@@ -1097,7 +1097,7 @@ let interp_refine ist gl rc =
   let kind = OfType (pf_concl gl) in
   let flags = {
     use_typeclasses = true;
-    use_unif_heuristics = true;
+    solve_unification_constraints = true;
     use_hook = None;
     fail_evar = false;
     expand_evars = true }
diff --git a/mathcomp/ssreflect/ssrmatching.v b/mathcomp/ssreflect/ssrmatching.v
deleted file mode 120000
index 0bf52be..0000000
--- a/mathcomp/ssreflect/ssrmatching.v
+++ /dev/null
@@ -1 +0,0 @@
-./plugin/v8.5/ssrmatching.v
-\ No newline at end of file
diff --git a/mathcomp/ssrmatching.v b/mathcomp/ssrmatching.v
deleted file mode 120000
index 4533fbb..0000000
--- a/mathcomp/ssrmatching.v
+++ /dev/null
@@ -1 +0,0 @@
-ssreflect/plugin/v8.5/ssrmatching.v
-\ No newline at end of file