From 75c99f5c048ff8dd7daf0d1692fa91f3ca8aeaff Mon Sep 17 00:00:00 2001
From: Talia Ringer
Date: Mon, 3 Jun 2019 10:54:59 -0400
Subject: Clean, document, and expand plugin tutorials 0 and 1

---
 doc/plugin_tutorial/tuto0/theories/Demo.v | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

(limited to 'doc/plugin_tutorial/tuto0/theories')

diff --git a/doc/plugin_tutorial/tuto0/theories/Demo.v b/doc/plugin_tutorial/tuto0/theories/Demo.v
index bdc61986af..54d5239421 100644
--- a/doc/plugin_tutorial/tuto0/theories/Demo.v
+++ b/doc/plugin_tutorial/tuto0/theories/Demo.v
@@ -1,8 +1,28 @@
 From Tuto0 Require Import Loader.
 
+(*** Printing messages ***)
+
 HelloWorld.
 
 Lemma test : True.
 Proof.
 hello_world.
 Abort.
+
+(*** Printing warnings ***)
+
+HelloWarning.
+
+Lemma test : True.
+Proof.
+hello_warning.
+Abort.
+
+(*** Signaling errors ***)
+
+Fail HelloError.
+
+Lemma test : True.
+Proof.
+Fail hello_error.
+Abort.
-- 
cgit v1.2.3