Skip to content
GitLab
Explore
Sign in
Hugo Herbelin
iris-coq
Repository
iris-coq
tests
proofmode.ref
Find file
Blame
History
Permalink
The Tactic Notation entry simple_intropattern now binds to Coq simple_intropattern.
· 51a9d973
Hugo Herbelin
authored
May 31, 2019
Formerly it was bound to Coq entry intropattern. See Coq PR#10239
51a9d973