aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/GibleSeq.v
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2022-06-03 18:08:05 +0100
committerYann Herklotz <git@yannherklotz.com>2022-06-03 18:08:05 +0100
commitdb4da00aea8b51bc9d90d83f981b9163eec3c540 (patch)
tree83d7f3bb6d8d70d7e7471917f1434cd2571a9c63 /src/hls/GibleSeq.v
parenta64b65a9f5b52372b413c31873fa14c3b1785b00 (diff)
downloadvericert-db4da00aea8b51bc9d90d83f981b9163eec3c540.tar.gz
vericert-db4da00aea8b51bc9d90d83f981b9163eec3c540.zip
Work on CondElim proof
Diffstat (limited to 'src/hls/GibleSeq.v')
-rw-r--r--src/hls/GibleSeq.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/GibleSeq.v b/src/hls/GibleSeq.v
index 30eb250..e66451d 100644
--- a/src/hls/GibleSeq.v
+++ b/src/hls/GibleSeq.v
@@ -32,7 +32,7 @@ Require Import vericert.hls.Gible.
(*|
========
-RTLBlock
+GibleSeq
========
|*)