doc/plugin_tutorial/tuto2/theories/Test.v


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

Declare ML Module "demo_plugin".

Cmd1.
Cmd2 With Some Terminal Parameters.
Cmd3 42.
Cmd4 100 200 300 400.
Cmd5 Foo_5.
Cmd5 Bar_5.
Cmd6.
Cmd7.
Cmd7.
Cmd7.

Goal True.
Proof.
  tactic1.
  tactic2 Foo_2.
  tactic2 Bar_2.
Abort.