Skip to content
GitLab
Explore
Sign in
Hugo Herbelin
iris-coq
Repository
Branches
Overview
Active
Stale
All
atomic
16cfe6ce
·
Use telescopes for atomic triples.
·
Nov 23, 2016
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
ci/debug
84444c51
·
Remove unused bound variable.
·
Dec 03, 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/janno/vmcast
caf434e7
·
Fix cast in `solve_as_val`.
·
Feb 27, 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
ci/ralf/pm_red
f02bf0d6
·
use beq instead of Bool.eqb in envs_replace
·
Jun 03, 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/stability
2f7efe5a
·
rerun CI
·
Jun 23, 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
fast_string
157e41c2
·
Use fast_string.
·
Feb 22, 2017
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
iris-3.0
0cc59b36
·
fix CI
·
Sep 16, 2017
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
janno/metacoq
3cc68b98
·
WIP generating mmatches.
·
Sep 25, 2017
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
jh/done_contradiction
8e3bb685
·
Trigger CI.
·
Feb 13, 2017
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
jh/evar_iframe
998bdedf
·
Get rid of KnownFrame and iFrame automatically instantiating evars.
·
Mar 03, 2018
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
jh/independent_metric
b863cfd7
·
Unbundle the inductives defining the metrics and equivalences of excl and csum.
·
Feb 08, 2017
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
jh/sprop_upred
111318cb
·
Upred is isomorphic to some kind of monotonous SProp predicate. (WIP)
·
Apr 04, 2017
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
jh_inductive_pairs
7d2a0390
·
Failed attempt at improving performances of pairs by using inductives
·
Jun 16, 2016
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
Prev
1
2
3
Next