diff options
| author | Yves Bertot | 2018-05-04 15:03:49 +0200 |
|---|---|---|
| committer | Yves Bertot | 2018-05-04 15:03:49 +0200 |
| commit | eba06e2192d88af463fb6dec85e2f039a0a13694 (patch) | |
| tree | a4773a4278bef687e4ba5b89e0e58ed6b6013539 /tuto1/src/simple_check.mli | |
| parent | dcdb59e6f51b11f9804ea0a9cd9566303df2c2b9 (diff) | |
finished type-checking examples
Diffstat (limited to 'tuto1/src/simple_check.mli')
| -rw-r--r-- | tuto1/src/simple_check.mli | 9 |
1 files changed, 8 insertions, 1 deletions
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 |