Add 'doc/plugin_tutorial/' from commit '168a13dab1c9987f592994150997e692d4d7e40b'

git-subtree-dir: doc/plugin_tutorial
git-subtree-mainline: 8c040974facb733682d24c488dc89941671f4ab7
git-subtree-split: 168a13dab1c9987f592994150997e692d4d7e40b

1 files changed, 17 insertions, 0 deletions

diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.ml b/doc/plugin_tutorial/tuto1/src/simple_print.ml
new file mode 100644
index 0000000000..cfc38ff9c9
--- /dev/null
+++ b/doc/plugin_tutorial/tuto1/src/simple_print.ml
@@ -0,0 +1,17 @@
+(* 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 _ ->
+    failwith "variables are not covered in this example"
+  | Globnames.IndRef _ ->
+    failwith "inductive types are not covered in this example"
+  | Globnames.ConstructRef _ ->
+    failwith "constructors are not covered in this example"
+  | Globnames.ConstRef cst ->
+    let cb = Environ.lookup_constant cst (Global.env()) in
+    match Global.body_of_constant_body cb with
+    | Some(e, _) -> e
+    | None -> failwith "This term has no value"
+