Merge pull request #19 from math-comp/mathcomp-1.9.0

Mathcomp 1.9.0

.travis.yml

@@ -17,6 +17,10 @@ env:
   - DOCKERIMAGE="mathcomp/mathcomp:1.8.0-coq-8.7"
   - DOCKERIMAGE="mathcomp/mathcomp:1.8.0-coq-8.8"
   - DOCKERIMAGE="mathcomp/mathcomp:1.8.0-coq-8.9"
+  - DOCKERIMAGE="mathcomp/mathcomp:1.9.0-coq-8.7"
+  - DOCKERIMAGE="mathcomp/mathcomp:1.9.0-coq-8.8"
+  - DOCKERIMAGE="mathcomp/mathcomp:1.9.0-coq-8.9"
+  - DOCKERIMAGE="mathcomp/mathcomp:1.9.0-coq-8.10"
 
 install: |
   # Prepare the COQ container

opam

@@ -10,7 +10,8 @@ license: "CeCILL-B"
 build: [ make "-j" "%{jobs}%" ]
 install: [ make "install" ]
 depends: [
-  "coq-mathcomp-field" { (>= "1.8.0" & < "1.9.0") }
+  "coq" { (>= "8.7" & < "8.11~") }
+  "coq-mathcomp-field" { (>= "1.8.0" & < "1.10.0~") }
   "coq-mathcomp-bigenough"   {(>= "1.0.0" & < "1.1.0~")}
 ]
 

shell.nix

@@ -0,0 +1,52 @@
+{withEmacs ? false,
+ nixpkgs ? (fetchTarball {
+  url = "https://github.com/NixOS/nixpkgs/archive/650a295621b27c4ebe0fa64a63fd25323e64deb3.tar.gz";
+  sha256 = "0rxjkfiq53ibz0rzggvnp341b6kgzgfr9x6q07m2my7ijlirs2da";
+}),
+coq-version ? "8.9",
+mc ? "1.8.0",
+print-env ? false
+}:
+let
+  config.packageOverrides = pkgs:
+    with pkgs; rec {
+      coqPackages =
+        let coqPackages = (with pkgs; {
+              "8.7" = coqPackages_8_7;
+              "8.8" = coqPackages_8_8;
+              "8.9" = coqPackages_8_9;
+              "8.10" = coqPackages_8_10;
+          }."${coq-version}");
+        in
+        coqPackages.overrideScope' (self: super: {
+          mathcompPkgs = if builtins.isString mc then (super.mathcompGen mc)
+                         else super.mathcomp.mathcompGen (o: {
+                            version = "dev";
+                            name = "coq${self.coq.coq-version}-mathcomp-custom";
+                            src = mc;
+             });
+           mathcomp = self.mathcompPkgs.all;
+           mathcomp-ssreflect = self.mathcompPkgs.ssreflect;
+           mathcomp-field = self.mathcompPkgs.field;
+       });
+       coq = coqPackages.coq;
+    };
+in
+with import nixpkgs {inherit config;};
+let
+  pgEmacs = emacsWithPackages (epkgs:
+    with epkgs.melpaStablePackages; [proof-general]);
+in
+stdenv.mkDerivation rec {
+  name = "env";
+  env = buildEnv { name = name; paths = buildInputs; };
+  buildInputs = [ coq ] ++ (with coqPackages; [mathcomp-field mathcomp-bigenough])
+                ++ lib.optional withEmacs pgEmacs;
+  shellHook = ''
+    nixEnv (){
+      echo "Here is your work environement:"
+      for x in $buildInputs; do printf "  "; echo $x | cut -d "-" -f "2-"; done
+      echo "you can pass option '--argstr coq-version \"x.y\"' to nix-shell to change coq versions"
+    }
+  '' + lib.optionalString print-env "nixEnv";
+}

theories/mxtens.v

@@ -51,7 +51,7 @@ Lemma mxtens_indexK m n : cancel (@mxtens_index m n) (@mxtens_unindex m n).
 Proof.
 case: m=> [[[] //]|m]; case: n=> [[_ [] //]|n].
 move=> [i j]; congr (_, _); apply: val_inj=> /=.
-  by rewrite divnMDl // divn_small.
+  by rewrite divnMDl // divn_small ?addn0.
 by rewrite modnMDl // modn_small.
 Qed.