Merge pull request #406 from ejgallego/v8.19+drop_mc_test_dep

Backports for 8.19.3

.github/workflows/ci.yml

@@ -41,7 +41,7 @@ jobs:
       matrix:
         ocaml-compiler: [4.09.x, 4.10.x, 4.11.x, 4.12.x, 4.13.x, 4.14.x]
         test-target: [test]
-        extra-opam: [coq.8.19.dev coq-mathcomp-ssreflect.1.dev]
+        extra-opam: [coq.8.19.dev]
         include:
         - ocaml-compiler: 4.13.1
           test-target: test
@@ -74,8 +74,6 @@ jobs:
           eval $(opam env)
           opam repos add coq-released http://coq.inria.fr/opam/released
           opam repos add coq-core-dev http://coq.inria.fr/opam/core-dev
-          # Only for mathcomp.dev which is needed for 8.16, remove when math-comp is fixed
-          opam repos add coq-extra-dev http://coq.inria.fr/opam/extra-dev
           # coq-serapi already pinned by the setup-ocaml@v2 action
           opam install --deps-only coq-serapi
       - name: Display OPAM Setup
@@ -98,12 +96,6 @@ jobs:
           ./configure -prefix "$HOME/coq-$COQ_BRANCH/_build/install/default/"
           make dunestrap
           dune build -p coq-core,coq-stdlib,coq
-          cd "$HOME"
-          # Install math-comp using Coq from git
-          PATH="$HOME/coq-$COQ_BRANCH/_build/install/default/bin:$PATH"
-          git clone --depth=3 -b mathcomp-1 https://github.com/math-comp/math-comp.git
-          make -C math-comp/mathcomp/ssreflect
-          make -C math-comp/mathcomp/ssreflect install
       - name: Extra OPAM Setup (Coq.dev, misc extra tools)
         if: ${{ matrix.extra-opam != '' }}
         run: |

CHANGES.md

@@ -1,3 +1,8 @@
+## Version 0.19.3
+
+ - [test] Don't require math-comp to run genarg tests (@ejgallego, #399 ,
+          fixes #395 , thanks to @SnarkBoojum for the report)
+
 ## Version 0.19.2
 
  - [serlib] Fix (@ejgallego, #398, fixes #397 fixes sr-lab/coqpyt#35 ,

coq-serapi.opam

@@ -36,16 +36,11 @@ depends: [
   "ppx_hash"            {           >= "v0.13.0"             }
   "yojson"              {           >= "1.7.0"               }
   "ppx_deriving_yojson" {           >= "3.4"                 }
-
-  # math-comp ssreflect is needed to run the tests.
-  #
-  # We can't enable this due to coq-mathcomp-ssreflect not being in
-  # the main opam repos, that would make opam's CI fail.
-  # "coq-mathcomp-ssreflect" { with-test & >= "1.15" }
 ]
 
 conflicts: [
   "result" {< "1.5"}
 ]
 
 build: [ "dune" "build" "-p" name "-j" jobs ]
+run-test: [ [ "dune" "runtest" "-p" name "-j" jobs ] ]

tests/genarg/move.v

@@ -1,9 +1,32 @@
 From Coq Require Import ssreflect ssrbool ssrfun.
-From mathcomp Require Import ssrnat eqtype.
+
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Module Equality.
+
+Definition axiom T (e : rel T) := forall x y, reflect (x = y) (e x y).
+
+Structure mixin_of T := Mixin {op : rel T; _ : axiom op}.
+Notation class_of := mixin_of (only parsing).
+
+Section ClassDef.
+
+Structure type := Pack {sort; _ : class_of sort}.
+Local Coercion sort : type >-> Sortclass.
+Variables (T : Type) (cT : type).
+
+Definition class := let: @Pack _ c := cT return class_of cT in c.
+
+Definition clone := fun c & cT -> T & phant_id (@Pack T c) cT => Pack c.
+
+End ClassDef.
+
+Definition eqType := Equality.type.
+Coercion Equality.sort : Equality.type >-> Sortclass.
+Notation EqType T m := (@Equality.Pack T m).
+
 Module Ordered.
 
 Section RawMixin.
@@ -27,7 +50,7 @@ Structure type : Type := Pack {sort : Type; _ : class_of sort;}.
 Local Coercion sort : type >-> Sortclass.
 
 Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Definition class := let: @Pack _ c as cT' := cT return class_of cT' in c.
 
 Definition pack b (m0 : mixin_of (EqType T b)) :=
   fun m & phant_id m0 m => Pack (@Class T b m).
@@ -45,6 +68,15 @@ End Exports.
 End Ordered.
 Export Ordered.Exports.
 
+Definition eq_op T := Equality.op (Equality.class T).
+
+Notation "x == y" := (eq_op x y)
+  (at level 70, no associativity) : bool_scope.
+
+Lemma eqP T : Equality.axiom (@eq_op T).
+Proof. by case: T => ? []. Qed.
+Arguments eqP {T x y}.
+
 Definition oleq (T : ordType) (t1 t2 : T) := ord t1 t2 || (t1 == t2).
 
 Prenex Implicits ord oleq.