diff options
| author | Yves Bertot | 2018-05-02 14:18:39 +0200 |
|---|---|---|
| committer | Yves Bertot | 2018-05-02 14:18:39 +0200 |
| commit | f893ebe4189bb2ecb085e6e139e13c9dadd4611a (patch) | |
| tree | 921478737eeb57c18114c3e9c8e8e3cf0cb2bd70 /tuto1/_CoqProject | |
| parent | 3df17ed7972dc404cc8519ae9bfd42f75e278e0b (diff) | |
first examples of commands taking arguments
Diffstat (limited to 'tuto1/_CoqProject')
| -rw-r--r-- | tuto1/_CoqProject | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/tuto1/_CoqProject b/tuto1/_CoqProject new file mode 100644 index 0000000000..7a191a961d --- /dev/null +++ b/tuto1/_CoqProject @@ -0,0 +1,5 @@ +-R theories/ Tuto0 +-I src + +src/g_tuto1.ml4 +src/tuto1_plugin.mlpack
\ No newline at end of file |