Merge pull request #8778 from SkySkimmer/merge-plugin-tuto

Move plugin tutorial to Coq repo

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"
+