From 2d647ce5fdf5343a7d9961a63d66b5191706aeaf Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 22 Mar 2022 16:43:39 +0000 Subject: Add comments to allow for literate detangling --- src/hls/RTLPargen.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'src/hls/RTLPargen.v') diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index ab4c0da..f3d13f5 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020-2021 Yann Herklotz + * Copyright (C) 2020-2022 Yann Herklotz * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by @@ -16,6 +16,7 @@ * along with this program. If not, see . *) +(* [[file:../../lit/scheduling.org::rtlpargen-main][rtlpargen-main]] *) Require Import compcert.backend.Registers. Require Import compcert.common.AST. Require Import compcert.common.Globalenvs. @@ -260,3 +261,4 @@ Definition transl_fundef := transf_partial_fundef transl_function. Definition transl_program (p : RTLBlock.program) : Errors.res RTLPar.program := transform_partial_program transl_fundef p. +(* rtlpargen-main ends here *) -- cgit