diff options
| -rw-r--r-- | tuto1/src/g_tuto1.ml4 | 2 | ||||
| -rw-r--r-- | tuto1/src/simple_print.ml | 3 |
2 files changed, 5 insertions, 0 deletions
diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.ml4 index 22bcfe8adb..b12ae3a073 100644 --- a/tuto1/src/g_tuto1.ml4 +++ b/tuto1/src/g_tuto1.ml4 @@ -1,3 +1,5 @@ +DECLARE PLUGIN "tuto1_plugin" + open Pp (* This one is necessary, to avoid message about missing wit_string *) open Stdarg diff --git a/tuto1/src/simple_print.ml b/tuto1/src/simple_print.ml index 5c4910d98e..cfc38ff9c9 100644 --- a/tuto1/src/simple_print.ml +++ b/tuto1/src/simple_print.ml @@ -1,3 +1,6 @@ +(* A more advanced example of how to explore the structure of terms of + type constr is given in the coq-dpdgraph plugin. *) + let simple_body_access gref = match gref with | Globnames.VarRef _ -> |