diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-12-17 10:03:30 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-12-17 10:03:30 +0000 |
| commit | 82b3cfa677c21e7d1fab907f1824bb101f819291 (patch) | |
| tree | 3be6d494b1da4562f36ac98ed43b5a016cb3f345 /src/SoftwarePipelining/SPTyping.mli | |
| parent | 51e3a17d2e65b095861c243807f4e8d76c60ea0e (diff) | |
| download | vericert-82b3cfa677c21e7d1fab907f1824bb101f819291.tar.gz vericert-82b3cfa677c21e7d1fab907f1824bb101f819291.zip | |
Modify software pipelining for build
Diffstat (limited to 'src/SoftwarePipelining/SPTyping.mli')
| -rw-r--r-- | src/SoftwarePipelining/SPTyping.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/SoftwarePipelining/SPTyping.mli b/src/SoftwarePipelining/SPTyping.mli index c231ddd..dd27875 100644 --- a/src/SoftwarePipelining/SPTyping.mli +++ b/src/SoftwarePipelining/SPTyping.mli @@ -11,5 +11,4 @@ -val type_function : RTL.coq_function -> unit - +(*val type_function : RTL.coq_function -> unit*) |