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/RTLPargenproof.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'src/hls/RTLPargenproof.v') diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index 0023edc..63a294e 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 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::rtlpargenproof-main][rtlpargenproof-main]] *) Require Import compcert.backend.Registers. Require Import compcert.common.AST. Require Import compcert.common.Errors. @@ -1135,3 +1136,4 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. Qed. End CORRECTNESS. +(* rtlpargenproof-main ends here *) -- cgit