diff options
| author | Yves Bertot | 2018-05-03 17:21:04 +0200 |
|---|---|---|
| committer | Yves Bertot | 2018-05-03 17:21:04 +0200 |
| commit | 3da6c143c9d9b8d419d5445f2ee906ca2e21648c (patch) | |
| tree | e9b20a155c985ba71ff0e90fa96603f822dee5e4 /tuto1/_CoqProject | |
| parent | f893ebe4189bb2ecb085e6e139e13c9dadd4611a (diff) | |
This version contains a simple command that defines a new constant
Diffstat (limited to 'tuto1/_CoqProject')
| -rw-r--r-- | tuto1/_CoqProject | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tuto1/_CoqProject b/tuto1/_CoqProject index 7a191a961d..3f087e48d7 100644 --- a/tuto1/_CoqProject +++ b/tuto1/_CoqProject @@ -1,5 +1,7 @@ --R theories/ Tuto0 +-R theories Tuto1 -I src +src/simple_declare.mli +src/simple_declare.ml src/g_tuto1.ml4 src/tuto1_plugin.mlpack
\ No newline at end of file |