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_declare.mli | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'doc/plugin_tutorial/tuto1/src/simple_declare.mli')

diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.mli b/doc/plugin_tutorial/tuto1/src/simple_declare.mli
index fd74e81526..c55b36742f 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.mli
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.mli
@@ -1,5 +1,4 @@
 open Names
-open EConstr
 
-val packed_declare_definition :
-    poly:bool -> Id.t -> constr Evd.in_evar_universe_context -> unit
+val declare_definition :
+    poly:bool -> Id.t -> Evd.evar_map -> EConstr.t -> Names.GlobRef.t
-- 
cgit v1.2.3