test-suite/misc/quotation_token/theories/quotation.v


1
2
3
4
5
6
7
8
9
10
11
12
13

Declare ML Module "quotation_plugin".

Definition x := foobar:{{ hello
  there
}}.

Definition y := foobar:{{ another
  multi line
  thing
}}.
Check foobar:{{ oops
 ips }} y.