diff options
| author | Gaëtan Gilbert | 2019-01-07 13:24:14 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-01-08 16:41:01 +0100 |
| commit | fde557d9e92d2ddd3c79d8a620f2cb33ce64a49f (patch) | |
| tree | 1b8a0e216119c908d50277432221ab06805a2ac9 /doc/plugin_tutorial/tuto1/src/simple_check.mli | |
| parent | 8c040974facb733682d24c488dc89941671f4ab7 (diff) | |
| parent | 168a13dab1c9987f592994150997e692d4d7e40b (diff) | |
Add 'doc/plugin_tutorial/' from commit '168a13dab1c9987f592994150997e692d4d7e40b'
git-subtree-dir: doc/plugin_tutorial
git-subtree-mainline: 8c040974facb733682d24c488dc89941671f4ab7
git-subtree-split: 168a13dab1c9987f592994150997e692d4d7e40b
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_check.mli')
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/simple_check.mli | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/doc/plugin_tutorial/tuto1/src/simple_check.mli b/doc/plugin_tutorial/tuto1/src/simple_check.mli new file mode 100644 index 0000000000..bcf1bf56cf --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/simple_check.mli @@ -0,0 +1,8 @@ +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 |