blob: 0efae6902f3b14537bcd2315b808f0fa8ccd6bd0 (
plain)
1
2
3
4
5
|
- **Added:**
Syntax :n:`injection @term as [= {+ @intropattern} ]` as
an alternative to :n:`injection @term as {+ @simple_intropattern}` using
the standard :n:`@injection_intropattern` syntax (`#9288
<https://github.com/coq/coq/pull/9288>`_, by Hugo Herbelin).
|
