Skip to content
GitLab
Explore
Sign in
Janno
iris-coq
Repository
Branches
Overview
Active
Stale
All
janno/iframe-cbv
8178efc8
·
iFrame: Do not call `cbv` on user terms in contexts
·
Mar 21, 2024
iris/iris!1042
janno/iframe-no-upd
609abd92
·
Prevent iFrame from instantiating existentials under updates.
·
Mar 12, 2024
iris/iris!1041
janno/fix-566
2618fee6
·
Add changelog entry.
·
Mar 06, 2024
iris/iris!1039
master
default
protected
5bb93f57
·
fix changelog typos
·
Feb 17, 2021
janno/try-HB
b109822a
·
Broken HB experiment.
·
May 22, 2020
ci/mtac2-tt
03e03b7f
·
cleanup CI script
·
Jul 23, 2019
very_important_renaming
5c756fec
·
Rename bi/lib/counter_examples to bi/lib/counterexamples.
·
Mar 20, 2019
iris/iris!226
ci/ralf/atomic
5bb0b874
·
remove unused Import
·
Jun 14, 2018
origin/ralf/coqbug/iAccu-anomaly
c1305d70
·
trigger an anomaly in Coq
·
Jun 14, 2018
gen_proofmode
8d3d9514
·
Merge branch 'ci/ralf/monpred-frame' into 'gen_proofmode'
·
Jun 14, 2018
ci/ralf/telescopes
e1688f08
·
Merge branch 'gen_proofmode' into ci/ralf/telescopes
·
Jun 14, 2018
ci/robbert/overloaded_wp
dbf83b1f
·
Typeclass to overload WP notation.
·
Jun 14, 2018
robbert/big_sepL2
051dfeae
·
Separating big operator over two lists.
·
Jun 14, 2018
ralf/reftests
8712401d
·
also test the output of error messages
·
Jun 10, 2018
ralf/pm_red
989bcb72
·
iApply: reduce after unifying lemma with goal
·
Jun 10, 2018
mtac2-tt
ffb1edea
·
Bump Mtac commit.
·
Jun 07, 2018
ci/ralf/pm_red
f02bf0d6
·
use beq instead of Bool.eqb in envs_replace
·
Jun 03, 2018
robbert/wp_misc
e5fb155f
·
Stronger version of adequacy that also talks about state.
·
May 29, 2018
ralf/emp-intro
15b4a65e
·
when the goal is an evar, pick emp when possible
·
Apr 20, 2018
joe/defined_pers
e472449d
·
Define persistently from the BI interface.
·
Mar 20, 2018
Prev
1
2
3
Next