aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto1/src/simple_check.mli
diff options
context:
space:
mode:
authorTalia Ringer2019-06-03 10:54:59 -0400
committerTalia Ringer2019-06-06 04:58:37 -0400
commit75c99f5c048ff8dd7daf0d1692fa91f3ca8aeaff (patch)
tree053c7aae588ef5cfaf2c2a3364c76922dcc23791 /doc/plugin_tutorial/tuto1/src/simple_check.mli
parent4f7af2b09a935528d660a354f5e7672fc92e9a5c (diff)
Clean, document, and expand plugin tutorials 0 and 1
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_check.mli')
-rw-r--r--doc/plugin_tutorial/tuto1/src/simple_check.mli7
1 files changed, 2 insertions, 5 deletions
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