diff options
| author | Enrico Tassi | 2016-11-08 10:53:17 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2016-11-08 10:53:17 +0100 |
| commit | 23e57fb47874331c5feaace883513b7abecdff28 (patch) | |
| tree | 5b4fcf12d0f0bb99716845d9094f0a550147d782 /mathcomp/ssreflect | |
| parent | 2a8af6f6b80c82a5f07cae220427cccc30ef8dac (diff) | |
fix compilation on 8.6 and trunk
Diffstat (limited to 'mathcomp/ssreflect')
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.6/ssreflect.ml4 | 2 | ||||
| l--------- | mathcomp/ssreflect/ssrmatching.v | 1 |
3 files changed, 2 insertions, 3 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 |