From 0a7f2f6f6e0f68a9fa89a27dc677b40f8dfb6e86 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 24 Jun 2022 18:28:41 +0100 Subject: Update documentation for Gible --- src/hls/GibleSeqgen.v | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'src/hls/GibleSeqgen.v') 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 . -=========== -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 -- cgit