From eba06e2192d88af463fb6dec85e2f039a0a13694 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Fri, 4 May 2018 15:03:49 +0200
Subject: finished type-checking examples

---
 tuto1/src/simple_check.mli | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

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

diff --git a/tuto1/src/simple_check.mli b/tuto1/src/simple_check.mli
index d745e68f6d..7079ca925d 100644
--- a/tuto1/src/simple_check.mli
+++ b/tuto1/src/simple_check.mli
@@ -1 +1,8 @@
-val simple_check : EConstr.constr Evd.in_evar_universe_context -> EConstr.constr
\ No newline at end of file
+val simple_check1 :
+  EConstr.constr Evd.in_evar_universe_context -> 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
\ No newline at end of file
-- 
cgit v1.2.3