From f506c2fa18c3dc67a19c7493e2d977ac8ee4668a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 14 Nov 2017 01:18:38 +0100
Subject: [PATCH] Use the version of ssreflect that's shipped with Coq 8.7.
---
.gitlab-ci.yml | 2 +-
opam | 3 +--
theories/algebra/base.v | 6 ++----
3 files changed, 4 insertions(+), 7 deletions(-)
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 63137a3da..1fa75c287 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -43,7 +43,7 @@ opam:
build-coq.8.7.dev:
<<: *template
variables:
- OPAM_PINS: "coq version 8.7.dev coq-mathcomp-ssreflect version dev"
+ OPAM_PINS: "coq version 8.7.dev"
artifacts:
paths:
- build-time.txt
diff --git a/opam b/opam
index 2f9b1ff11..84f0313fb 100644
--- a/opam
+++ b/opam
@@ -10,7 +10,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
- "coq" { >= "8.6.1" & < "8.8~" }
- "coq-mathcomp-ssreflect" { (>= "1.6.1" & < "1.7~") | (= "dev") }
+ "coq" { >= "8.7.0" & < "8.8~" }
"coq-stdpp" { (= "dev.2017-11-12.2") | (= "dev") }
]
diff --git a/theories/algebra/base.v b/theories/algebra/base.v
index 79f8e4978..603e9c20c 100644
--- a/theories/algebra/base.v
+++ b/theories/algebra/base.v
@@ -1,8 +1,6 @@
-From mathcomp Require Export ssreflect.
+From Coq.ssr Require Export ssreflect.
From stdpp Require Export prelude.
Set Default Proof Using "Type".
-(* Reset options set by the ssreflect plugin to their defaults *)
-Global Set Bullet Behavior "Strict Subproofs".
Global Open Scope general_if_scope.
-Global Unset Asymmetric Patterns.
+Global Set SsrOldRewriteGoalsOrder. (* See Coq issue #5706 *)
Ltac done := stdpp.tactics.done.
--
GitLab