From 23e57fb47874331c5feaace883513b7abecdff28 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 8 Nov 2016 10:53:17 +0100
Subject: fix compilation on 8.6 and trunk

---
 mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 2 +-
 mathcomp/ssreflect/plugin/v8.6/ssreflect.ml4  | 2 +-
 mathcomp/ssreflect/ssrmatching.v              | 1 -
 3 files changed, 2 insertions(+), 3 deletions(-)
 delete mode 120000 mathcomp/ssreflect/ssrmatching.v

(limited to 'mathcomp/ssreflect')

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