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 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'mathcomp/ssreflect/plugin/trunk') 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 } -- cgit v1.2.3