bug_11549.v « closed « bugs « test-suite - coq - The formal proof system

about summary refs log tree commit diff

path: root/test-suite/bugs/closed/bug_11549.v

blob: 7608e1c4d823ebd7f6327d41032c5d207ba09fb1 (plain)

From Ltac2 Require Ltac2.

Notation "t $ r" := (t r)
  (at level 65, right associativity, only parsing).
Check S $ O.