diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-03-23 09:47:56 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-03-23 09:47:56 +0000 |
| commit | f00a195ac17fe47047fafc183663a96ec4125f0d (patch) | |
| tree | f0c535c0e0b911abb8cf8f6738ee9a05d9d09971 /src/hls/RTLBlockgen.v | |
| parent | 6b2e01e97ca67219465b92e0fbe536bf2a5434e7 (diff) | |
| download | vericert-f00a195ac17fe47047fafc183663a96ec4125f0d.tar.gz vericert-f00a195ac17fe47047fafc183663a96ec4125f0d.zip | |
Change origin of tangled files
Diffstat (limited to 'src/hls/RTLBlockgen.v')
| -rw-r--r-- | src/hls/RTLBlockgen.v | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/src/hls/RTLBlockgen.v b/src/hls/RTLBlockgen.v index fa462e7..6d38e4f 100644 --- a/src/hls/RTLBlockgen.v +++ b/src/hls/RTLBlockgen.v @@ -16,7 +16,7 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -(* [[file:../../lit/scheduling.org::rtlblockgen-imports][rtlblockgen-imports]] *) +(* [[file:../../lit/basic-block-generation.org::rtlblockgen-imports][rtlblockgen-imports]] *) Require compcert.backend.RTL. Require Import compcert.common.AST. Require Import compcert.lib.Maps. @@ -30,7 +30,6 @@ Require Import vericert.hls.RTLBlock. #[local] Open Scope positive. (* rtlblockgen-imports ends here *) -(* [[file:../../lit/scheduling.org::rtlblockgen-equalities-insert][rtlblockgen-equalities-insert]] *) Lemma comparison_eq: forall (x y : comparison), {x = y} + {x <> y}. Proof. decide equality. @@ -148,9 +147,8 @@ Defined. Definition ceq {A: Type} (eqd: forall a b: A, {a = b} + {a <> b}) (a b: A): bool := if eqd a b then true else false. -(* rtlblockgen-equalities-insert ends here *) -(* [[file:../../lit/scheduling.org::rtlblockgen-main][rtlblockgen-main]] *) +(* [[file:../../lit/basic-block-generation.org::rtlblockgen-main][rtlblockgen-main]] *) Parameter partition : RTL.function -> Errors.res function. (** [find_block max nodes index]: Does not need to be sorted, because we use filter and the max fold |