Merge pull request #26 from certichain/mathcomp-1.9-fix

Mathcomp 1.9.0 compatibility

.travis.yml

@@ -12,7 +12,7 @@ opam: &OPAM
       export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m '
       set -ex  # -e = exit on failure; -x = trace for debug
       opam update -y
-      opam pin add ${CONTRIB_NAME} . -y --no-action
+      opam pin add ${CONTRIB_NAME} . -y -n -k path
       opam install ${CONTRIB_NAME} -y -j ${NJOBS} --deps-only
       opam config list
       opam repo list
@@ -39,6 +39,11 @@ matrix:
     - CONTRIB_NAME=coq-toychain
     - NJOBS=2
     <<: *OPAM
+  - env:
+    - COQ_IMAGE=coqorg/coq:8.10
+    - CONTRIB_NAME=coq-toychain
+    - NJOBS=2
+    <<: *OPAM
   - env:
     - COQ_IMAGE=coqorg/coq:dev
     - CONTRIB_NAME=coq-toychain

Extraction/Impl.v

@@ -167,7 +167,7 @@ case: ifP; last first.
 
 (* When total work is equal, LHS is longer *)
 - case: ifP;
-  have X: (Datatypes.length bc + 0 = Datatypes.length bc) by [].
+  have X: (Datatypes.length bc + 0 = Datatypes.length bc) by rewrite ?addn0.
   by rewrite List.app_length -{2}X eqn_add2l.
   by move=>_ _; rewrite -PeanoNat.Nat.ltb_antisym List.app_length -{1}X;
      apply/PeanoNat.Nat.ltb_lt/ltP; rewrite ltn_add2l.
@@ -247,7 +247,7 @@ move=>bc bc'; rewrite/subchain/FCR; move=>[fs][ls]=>->; case: ifP.
   + case: ifP; first by move/eqP=>->; left.
     move=>A; rewrite !List.app_length.
     rewrite PeanoNat.Nat.add_comm Plus.plus_assoc_reverse.
-    have X: (Datatypes.length bc + 0 = Datatypes.length bc) by [].
+    have X: (Datatypes.length bc + 0 = Datatypes.length bc) by rewrite ?addn0.
     rewrite -{2}X.
     move/eqP/(Plus.plus_reg_l (Datatypes.length ls + Datatypes.length fs)%coq_nat
                               0 (Datatypes.length bc)).
@@ -258,7 +258,7 @@ move=>bc bc'; rewrite/subchain/FCR; move=>[fs][ls]=>->; case: ifP.
     rewrite -!PeanoNat.Nat.ltb_antisym !List.app_length;
     rewrite {1 2}PeanoNat.Nat.add_comm !Plus.plus_assoc_reverse=>A.
     apply/PeanoNat.Nat.ltb_spec0; apply: PeanoNat.Nat.lt_add_pos_r.
-    have X: (Datatypes.length bc + 0 = Datatypes.length bc) by [].
+    have X: (Datatypes.length bc + 0 = Datatypes.length bc) by rewrite ?addn0.
     move: A; rewrite -{2}X; clear X.
     case Z: ((Datatypes.length ls + Datatypes.length fs)%coq_nat == 0).
     by move/eqP: Z=>->; rewrite eq_refl.

coq-toychain-node.opam

@@ -1,5 +1,4 @@
 opam-version: "2.0"
-version: "dev"
 maintainer: "[email protected]"
 
 homepage: "https://github.com/certichain/toychain"
@@ -11,8 +10,8 @@ synopsis: "Blockchain node extracted from verified minimalistic protocol"
 build: [ make "-j%{jobs}%" "node" ]
 depends: [
   "ocaml"
-  "coq" {(>= "8.9" & < "8.10~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {(>= "1.7" & < "1.9~") | (= "dev")}
+  "coq" {(>= "8.9" & < "8.11~") | (= "dev")}
+  "coq-mathcomp-ssreflect" {(>= "1.7" & < "1.10~") | (= "dev")}
   "coq-fcsl-pcm"
   "ocamlbuild" {build}
   "cryptokit"

coq-toychain.opam

@@ -1,5 +1,4 @@
 opam-version: "2.0"
-version: "dev"
 maintainer: "[email protected]"
 
 homepage: "https://github.com/certichain/toychain"
@@ -12,8 +11,8 @@ build: [ make "-j%{jobs}%" ]
 install: [ make "install" ]
 depends: [
   "ocaml"
-  "coq" {(>= "8.9" & < "8.10~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {(>= "1.7" & < "1.9~") | (= "dev")}
+  "coq" {(>= "8.9" & < "8.11~") | (= "dev")}
+  "coq-mathcomp-ssreflect" {(>= "1.7" & < "1.10~") | (= "dev")}
   "coq-fcsl-pcm"
 ]