Skip to content
GitLab
Explore
Sign in
Hugo Herbelin
iris-coq
Repository
Branches
Overview
Active
Stale
All
master+adapt-coq-pr12950-notation-registering-reworking
84f3f086
·
Compatibility with Coq PR #12984 about new reimport of printing rules.
·
Oct 24, 2020
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
master+adapt-coq11327-coercion-funclass-inherit-implicit
5f82722e
·
Adapt to Coq PR #11327 (coercions to funclass inherit implicit arguments).
·
Feb 18, 2020
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
master+adapt-coq-pr11261-dont-print-implicit-types
5712dba8
·
Adapting to Coq PR #11261: do not print types of variables with implicit types.
·
Feb 18, 2020
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
master+fix-interpretation-notation-format-pr10832
33272af5
·
Adapting to Coq PR#10832: formats associated to a given interpretation
·
Nov 12, 2019
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
master+consequence-coq-pr10239-intropattern-means-simple_intropattern
51a9d973
·
The Tactic Notation entry simple_intropattern now binds to Coq simple_intropattern.
·
May 31, 2019
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
master
default
protected
04df38b7
·
Merge branch 'robbert/ufrac_just_ufrac' into 'master'
·
Dec 21, 2018
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
robbert/ufrac
1d67a47f
·
The unbounded fractional authoritative camera.
·
Dec 20, 2018
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
mtac2-tt
03a692fa
·
update Makefile and CI config
·
Dec 19, 2018
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
ci/debug
84444c51
·
Remove unused bound variable.
·
Dec 03, 2018
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
robbert/plausibly
3e4b87c2
·
Show that bupd entails plausibly.
·
Oct 27, 2018
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
robbert/bupd_be_gone
d3814459
·
Remove basic updates from the Iris model, and define them using plainly.
·
Oct 27, 2018
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
joe/fupd_extra
818a8dfa
·
Show that step fupd commutes with forall for plain predicates in Iris.
·
Oct 24, 2018
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
ci/value_constructor
8897df8d
·
Move `Atomic`, `IntoVal` and `AsVal` instances to lifting.
·
Oct 22, 2018
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
ci/robbert/into_val_pures
ae5de30b
·
Allow `IntoVal` to take pure steps.
·
Oct 18, 2018
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
ci/janno/debug-opam
0b532336
·
Switch to iris-ci/debug.
·
Oct 10, 2018
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
ci/ralf/ci
4225335f
·
write URLs the way opam writes them
·
Oct 01, 2018
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
iris-3.1
a9a865a9
·
use Docker image matching CI branch
·
Sep 19, 2018
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
ci/3.1.0
2ab25b8a
·
Address Ralf's feedback in .gitlab-ci.yml.
·
Aug 31, 2018
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
joe/bupd_derived
cf2c0829
·
Show that bupd can be (essentially) defined in terms of other connectives.
·
Aug 17, 2018
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
ralf/later-normal
c9d23da2
·
rely on normalization for laterN
·
Jul 03, 2018
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
Prev
1
2
3
Next