From c2658eb76dbd4e616bfb449566fa6645f63777ed Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Fri, 4 May 2018 17:46:28 +0200
Subject: adds an explanation to Cmd8

---
 tuto1/src/g_tuto1.ml4 | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.ml4
index b12ae3a073..e71c880d01 100644
--- a/tuto1/src/g_tuto1.ml4
+++ b/tuto1/src/g_tuto1.ml4
@@ -108,6 +108,11 @@ VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY
          (Simple_check.simple_check3 v)) ]
 END
 
+(* This command takes a name and return its value.  It does less
+  than Print, because it fails on constructors, axioms, and inductive types.
+  This should be improved, because the error message is an anomaly.
+  Anomalies should never appear even when using a command outside of its
+  intended use. *)
 VERNAC COMMAND EXTEND ExamplePrint CLASSIFIED AS QUERY
 | [ "Cmd8" reference(r) ] ->
   [ let env = Global.env() in
-- 
cgit v1.2.3