diff options
| author | Yves Bertot | 2018-05-04 17:46:28 +0200 |
|---|---|---|
| committer | Yves Bertot | 2018-05-04 17:46:28 +0200 |
| commit | c2658eb76dbd4e616bfb449566fa6645f63777ed (patch) | |
| tree | 0053efddadd69d1a03a55dd9ae698fa88b6cee23 | |
| parent | dd660f27e2ff7247a52c1f80a7fc1b6cc286bae5 (diff) | |
adds an explanation to Cmd8
| -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 |