From 75c99f5c048ff8dd7daf0d1692fa91f3ca8aeaff Mon Sep 17 00:00:00 2001
From: Talia Ringer
Date: Mon, 3 Jun 2019 10:54:59 -0400
Subject: Clean, document, and expand plugin tutorials 0 and 1

---
 doc/plugin_tutorial/tuto1/src/simple_print.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/plugin_tutorial/tuto1/src/simple_print.ml')

diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.ml b/doc/plugin_tutorial/tuto1/src/simple_print.ml
index 22a0163fbb..48b5f2214c 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_print.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_print.ml
@@ -12,6 +12,6 @@ let simple_body_access gref =
   | Globnames.ConstRef cst ->
     let cb = Environ.lookup_constant cst (Global.env()) in
     match Global.body_of_constant_body Library.indirect_accessor cb with
-    | Some(e, _) -> e
+    | Some(e, _) -> EConstr.of_constr e
     | None -> failwith "This term has no value"
 
-- 
cgit v1.2.3