add support for analysis 0.3.9

affeldt-aist · Jun 17, 2021 · 645ff82 · 645ff82
1 parent 662931d
commit 645ff82
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 6 deletions.
diff --git a/coq-monae.opam b/coq-monae.opam
@@ -24,7 +24,7 @@ depends: [
   "coq-mathcomp-algebra" { (>= "1.12.0" & < "1.13~") }
   "coq-mathcomp-solvable" { (>= "1.12.0" & < "1.13~") }
   "coq-mathcomp-field" { (>= "1.12.0" & < "1.13~") }
-  "coq-mathcomp-analysis" { (>= "0.3.6" & <= "0.3.7") }
+  "coq-mathcomp-analysis" { (>= "0.3.6" & <= "0.3.7") | (>= "0.3.9" & < "0.4~") }
   "coq-infotheo" { >= "0.3.2" & < "0.4~"}
   "coq-paramcoq" { >= "1.1.2" & < "1.2~" }
 ]

diff --git a/gcm_model.v b/gcm_model.v
@@ -389,8 +389,7 @@ move=> p a0 a1; apply necset_ext => /=; rewrite predeqE => b0; split.
 - rewrite !necset_convType.convE.
   case=> a [] a0' a0a0'; rewrite conv_pt_setE=> -[] a1' a1a1' <- <- /=.
   by case: f=> f' /= ->; apply conv_in_conv_set; apply imageP.
-
-- rewrite !necset_convType.convE /= => /conv_in_conv_set' [] x [] y [] [] a0' a0a0' <- [] [] a1' a1a1' <- ->.
+- rewrite !necset_convType.convE => /conv_in_conv_set' [] x [] y [] [] a0' a0a0' <- [] [] a1' a1a1' <- ->.
   rewrite affine_image_conv_set /=.
   by apply conv_in_conv_set; apply imageP.
 Qed.

diff --git a/meta.yml b/meta.yml
@@ -68,7 +68,7 @@ dependencies:
     [MathComp field](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-analysis
-    version: '{ (>= "0.3.6" & <= "0.3.7") }'
+    version: '{ (>= "0.3.6" & <= "0.3.7") | (>= "0.3.9" & < "0.4~") }'
   description: |-
     [MathComp analysis](https://github.com/math-comp/analysis)
 - opam:

diff --git a/monad_model.v b/monad_model.v
@@ -144,11 +144,12 @@ End ListMonad.
 
 Module SetMonad.
 Section setmonad.
-Lemma map_id : FunctorLaws.id (@image).
+Local Open Scope classical_set_scope.
+Lemma map_id : FunctorLaws.id (fun T1 T2 f A => f @` A).
 Proof.
 by move=> x; rewrite boolp.funeqE => y; rewrite image_id.
 Qed.
-Lemma map_comp : FunctorLaws.comp (@image).
+Lemma map_comp : FunctorLaws.comp (fun T1 T2 f A => f @` A).
 Proof.
 by move=> A B C g h; rewrite boolp.funeqE => x /=; rewrite image_comp.
 Qed.