diff options
Diffstat (limited to 'doc/plugin_tutorial/tuto2/theories/Count.v')
| -rw-r--r-- | doc/plugin_tutorial/tuto2/theories/Count.v | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/doc/plugin_tutorial/tuto2/theories/Count.v b/doc/plugin_tutorial/tuto2/theories/Count.v new file mode 100644 index 0000000000..3287342b75 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/theories/Count.v @@ -0,0 +1,19 @@ +Require Import Demo. + +(*** Local ***) + +Count. +Count. + +Import Demo. + +Count. + +(*** Persistent ***) + +Count Persistent. +Count Persistent. + +Import Demo. + +Count Persistent. |