diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
index f4e2ac8d57..72161e7396 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 1e122ea855..6aaa79b509 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 0bf52beba2..0000000000
--- 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 4533fbba40..0000000000
--- a/mathcomp/ssrmatching.v
+++ /dev/null
@@ -1 +0,0 @@
-ssreflect/plugin/v8.5/ssrmatching.v
\ No newline at end of file