Skip to content
GitLab
Projects
Groups
Topics
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Marianna Rapoport
iris-coq
Repository
iris-coq
proofmode
intro_patterns.v
Find file
Blame
History
Permalink
Enable $-prefixes in ssr-like {H1 .. Hn} intro-patterns to perform framing.
· a9f8d0f0
Robbert Krebbers
authored
Jun 30, 2016
For example iIntros "{$H1 H2} H1" frames H1, clears H2, and introduces H1.
a9f8d0f0
