diff options
| author | Yves Bertot | 2018-05-04 09:12:06 +0200 |
|---|---|---|
| committer | Yves Bertot | 2018-05-04 09:12:06 +0200 |
| commit | 673f55be2b5139f154bbd84e72550a7c7c58341a (patch) | |
| tree | eb99108b50cf88f0fc33680f3c967fc2282132c1 /tuto1/src/simple_check.mli | |
| parent | 93273e29708ff5c24024bde0e4b9955cb94a0dc0 (diff) | |
This revision contains a simple Check command.
Diffstat (limited to 'tuto1/src/simple_check.mli')
| -rw-r--r-- | tuto1/src/simple_check.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tuto1/src/simple_check.mli b/tuto1/src/simple_check.mli new file mode 100644 index 0000000000..d745e68f6d --- /dev/null +++ b/tuto1/src/simple_check.mli @@ -0,0 +1 @@ +val simple_check : EConstr.constr Evd.in_evar_universe_context -> EConstr.constr
\ No newline at end of file |