From 2f5fefcd76259d5e0aee5ef5076ae4c4dd662ec1 Mon Sep 17 00:00:00 2001 From: Talia Ringer Date: Fri, 7 Jun 2019 06:59:16 -0400 Subject: Update, expand, and document plugin tutorial 2 --- doc/plugin_tutorial/tuto2/theories/Count.v | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 doc/plugin_tutorial/tuto2/theories/Count.v (limited to 'doc/plugin_tutorial/tuto2/theories/Count.v') 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. -- cgit v1.2.3