1 files changed, 6 insertions, 4 deletions
diff --git a/src/hls/GibleSeqgen.v b/src/hls/GibleSeqgen.v
index 31dabf8..127ee53 100644
--- a/src/hls/GibleSeqgen.v
+++ b/src/hls/GibleSeqgen.v
@@ -16,10 +16,6 @@
    You should have received a copy of the GNU General Public License
    along with this program.  If not, see <https://www.gnu.org/licenses/>.
 
-===========
-RTLBlockgen
-===========
-
 .. coq:: none
 |*)
 
@@ -36,6 +32,12 @@ Require Import vericert.hls.GibleSeq.
 
 #[local] Open Scope positive.
 
+(*|
+====================
+Gible Seq Generation
+====================
+|*)
+
 Definition check_valid_node (tc: code) (e: node) :=
   match tc ! e with
   | Some _ => true