diff options
| author | Yves Bertot | 2018-05-04 17:35:17 +0200 |
|---|---|---|
| committer | Yves Bertot | 2018-05-04 17:35:17 +0200 |
| commit | 6e9ee6b1cd9290951fe1f53bbb28f313aca45712 (patch) | |
| tree | 481bdec086e20806bdd256c4e00e536673f3763b | |
| parent | 3365fb1c5fa3d37f23775e7fb3ee4a2a341bb2ef (diff) | |
adds a comment in simple_print.ml and a plugin declaration in g_tuto1.ml4
| -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 _ -> |