Skip to content
Snippets Groups Projects
Select Git revision
  • janno/ipm-strings-upstream
  • janno/ipm-strings
  • janno/iframe-cbv
  • janno/iframe-no-upd
  • janno/fix-566
  • master default protected
  • janno/try-HB
  • ci/mtac2-tt
  • very_important_renaming
  • ci/ralf/atomic
  • origin/ralf/coqbug/iAccu-anomaly
  • gen_proofmode
  • ci/ralf/telescopes
  • ci/robbert/overloaded_wp
  • robbert/big_sepL2
  • ralf/reftests
  • ralf/pm_red
  • mtac2-tt
  • ci/ralf/pm_red
  • robbert/wp_misc
  • iris-3.1.0
  • iris-3.0.0
  • iris-2.0
  • iris-2.0-rc2
  • iris-2.0-rc1
  • iris-1.1
  • iris-1.0
  • hope-2015-coq-1
  • appendix-1.0.0
  • appendix-1
30 results
Compare
Forked from Iris / Iris
Source project has a limited visibility.
user avatar
Support `iIntros "ipat" (x1 .. xn) "ipat".
Robbert Krebbers authored 
This makes it easier to frame or introduce some modalities before introducing
universal quantifiers.
437b700f
History
user avatar 437b700f
History
Name Last commit Last update