Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
I
iris-coq
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Service Desk
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Marianna Rapoport
iris-coq
Commits
ccb21344
Commit
ccb21344
authored
Apr 18, 2018
by
Ralf Jung
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
drop support for Coq 8.6; use the ssreflect that ships with Coq
parent
1c09a14c
Changes
4
Hide whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
11 additions
and
18 deletions
+11
-18
.gitlab-ci.yml
.gitlab-ci.yml
+5
-10
README.md
README.md
+3
-2
opam
opam
+1
-2
theories/algebra/base.v
theories/algebra/base.v
+2
-4
No files found.
.gitlab-ci.yml
View file @
ccb21344
...
...
@@ -29,13 +29,13 @@ variables:
build-coq.dev
:
<<
:
*template
variables
:
OPAM_PINS
:
"
coq
version
dev
coq-mathcomp-ssreflect
version
dev
"
OPAM_PINS
:
"
coq
version
dev"
VALIDATE
:
"
1"
build-coq.8.7.2
:
<<
:
*template
variables
:
OPAM_PINS
:
"
coq
version
8.7.2
coq-mathcomp-ssreflect
version
1.6.4
"
OPAM_PINS
:
"
coq
version
8.7.2"
OPAM_PKG
:
"
coq-iris"
TIMING_PROJECT
:
"
iris"
TIMING_CONF
:
"
coq-8.7.2"
...
...
@@ -45,22 +45,17 @@ build-coq.8.7.2:
build-coq.8.7.1
:
<<
:
*template
variables
:
OPAM_PINS
:
"
coq
version
8.7.1
coq-mathcomp-ssreflect
version
1.6.4
"
OPAM_PINS
:
"
coq
version
8.7.1"
build-coq.8.7.0
:
<<
:
*template
variables
:
OPAM_PINS
:
"
coq
version
8.7.0
coq-mathcomp-ssreflect
version
1.6.4"
build-coq.8.6.1
:
<<
:
*template
variables
:
OPAM_PINS
:
"
coq
version
8.6.1
coq-mathcomp-ssreflect
version
1.6.4"
OPAM_PINS
:
"
coq
version
8.7.0"
build-stdpp.dev
:
<<
:
*template
variables
:
OPAM_PINS
:
"
coq
version
8.7.2
coq-
mathcomp-ssreflect
version
1.6.4
coq-
stdpp.dev
git
https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/#$STDPP_REV"
OPAM_PINS
:
"
coq
version
8.7.2
coq-stdpp.dev
git
https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/#$STDPP_REV"
except
:
only
:
-
triggers
...
...
README.md
View file @
ccb21344
...
...
@@ -6,10 +6,11 @@ This is the Coq development of the [Iris Project](http://iris-project.org).
This version is known to compile with:
-
Coq 8.6.1 / 8.7.0 / 8.7.1 / 8.7.2
-
Ssreflect 1.6.4
-
Coq 8.7.0 / 8.7.1 / 8.7.2
-
A development version of
[
std++
](
https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp
)
For a version compatible with Coq 8.6, have a look at the
[
iris-3.1 branch
](
https://gitlab.mpi-sws.org/FP/iris-coq/tree/iris-3.1
)
.
If you need to work with Coq 8.5, please check out the
[
iris-3.0 branch
](
https://gitlab.mpi-sws.org/FP/iris-coq/tree/iris-3.0
)
.
...
...
opam
View file @
ccb21344
...
...
@@ -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~") | (= "dev") }
"coq-mathcomp-ssreflect" { (>= "1.6.1" & < "1.7~") | (= "dev") }
"coq" { (>= "8.7.0" & < "8.8~") | (= "dev") }
"coq-stdpp" { (= "dev.2018-04-11.0") | (= "dev") }
]
theories/algebra/base.v
View file @
ccb21344
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
.
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment