fix compilation on 8.6 and trunk

math-comp · Nov 8, 2016 · 23e57fb · 23e57fb
1 parent 2a8af6f
commit 23e57fb
Show file tree

Hide file tree

Showing 4 changed files with 2 additions and 4 deletions.
diff --git 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
@@ -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
diff --git a/mathcomp/ssrmatching.v b/mathcomp/ssrmatching.v