diff options
| -rw-r--r-- | tuto1/src/g_tuto1.ml4 | 5 |
1 files changed, 5 insertions, 0 deletions
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 |