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/algebra/matrix.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'mathcomp/algebra') diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index f87fb78..2580741 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -215,7 +215,7 @@ Definition mx_val A := let: Matrix g := A in g. Canonical matrix_subType := Eval hnf in [newType for mx_val]. Fact matrix_key : unit. Proof. by []. Qed. -Definition matrix_of_fun_def F := Matrix [ffun ij => F ij.1 ij.2 : R]. +Definition matrix_of_fun_def F := Matrix [ffun ij => F ij.1 ij.2]. Definition matrix_of_fun k := locked_with k matrix_of_fun_def. Canonical matrix_unlockable k := [unlockable fun matrix_of_fun k]. @@ -277,8 +277,7 @@ Notation "\row_ ( j < n ) E" := (@matrix_of_fun _ 1 n matrix_key (fun _ j => E)) Notation "\row_ j E" := (\row_(j < _) E) : ring_scope. Definition matrix_eqMixin (R : eqType) m n := - @SubEqMixin (@finfun_eqType _ (fun=> _)) _ (matrix_subType R m n). -(* Eval hnf in [eqMixin of 'M[R]_(m, n) by <:]. *) + Eval hnf in [eqMixin of 'M[R]_(m, n) by <:]. Canonical matrix_eqType (R : eqType) m n:= Eval hnf in EqType 'M[R]_(m, n) (matrix_eqMixin R m n). Definition matrix_choiceMixin (R : choiceType) m n := -- cgit v1.2.3