From c5763504783b51bb5def88c82f55a0b99ebf9d67 Mon Sep 17 00:00:00 2001
From: Georges Gonthier
Date: Mon, 4 Mar 2019 11:49:56 +0100
Subject: Compatibility fix for Coq issue coq/#9663

Coq currently fails to resolve Miller patterns against open evars
(issue coq/#9663), in particular it fails to unify `T -> ?R` with
`forall x : T, ?dR x` even when `?dR` does not have `x` in its context.
As a result canonical structures and constructor notations for the
new generalised dependent `finfun`s fail for the non-dependent use
cases, which is an unacceptable regression.
This commit mitigates the problem by specialising the canonical
instances and most of the constructor notation to the non-dependent
case, and introducing an alias of the `finfun_of` type that has
canonical instances for the dependent case, to allow experimentation
with that feature.
With this fix the whole `MathComp` library compiles, with a few
minor changes. The change in `integral_char` fixes a performance issue
that appears to be the consequence of insufficient locking of both
`finfun_eqType` and `cfIirr`; this will be explored in a further commit.
---
 mathcomp/solvable/burnside_app.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp/solvable')

diff --git a/mathcomp/solvable/burnside_app.v b/mathcomp/solvable/burnside_app.v
index 34c1c7c..f5f3719 100644
--- a/mathcomp/solvable/burnside_app.v
+++ b/mathcomp/solvable/burnside_app.v
@@ -694,8 +694,8 @@ Proof. by move=> p1 p2 /val_inj/(can_inj fgraphK)/val_inj. Qed.
 Definition prod_tuple (t1 t2 : seq cube) :=
   map (fun n : 'I_6 => nth F0 t2 n) t1.
 
-Lemma sop_spec : forall x (n0 : 'I_6), nth F0 (sop x) n0 = x n0.
-Proof. by move=> x n0; rewrite -pvalE unlock enum_rank_ord (tnth_nth F0). Qed.
+Lemma sop_spec x (n0 : 'I_6): nth F0 (sop x) n0 = x n0.
+Proof. by rewrite nth_fgraph_ord pvalE. Qed.
 
 Lemma prod_t_correct : forall (x y : {perm cube}) (i : cube),
   (x * y) i = nth F0 (prod_tuple (sop x) (sop y)) i.
-- 
cgit v1.2.3