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

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

diff --git a/doc/plugin_tutorial/tuto1/src/simple_check.mli b/doc/plugin_tutorial/tuto1/src/simple_check.mli
index bcf1bf56cf..4b28ac74fe 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_check.mli
+++ b/doc/plugin_tutorial/tuto1/src/simple_check.mli
@@ -1,8 +1,5 @@
 val simple_check1 :
-  EConstr.constr Evd.in_evar_universe_context -> EConstr.constr
+  Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr
 
 val simple_check2 :
-  EConstr.constr Evd.in_evar_universe_context -> Evd.evar_map * EConstr.constr
-
-val simple_check3 :
-  EConstr.constr Evd.in_evar_universe_context -> EConstr.constr
+  Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr
-- 
cgit v1.2.3