diff options
author | Yann Herklotz <git@yannherklotz.com> | 2022-03-24 10:04:47 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2022-03-24 10:04:47 +0000 |
commit | 4b012187df7c66bef2300252058f27ac79337325 (patch) | |
tree | c9fa8c54725ab2126b59199a7718ff241b78121f /src/hls/RTLBlockgen.v | |
parent | 9eeb3845eb466189276fb16e08c41902b430c342 (diff) | |
download | vericert-4b012187df7c66bef2300252058f27ac79337325.tar.gz vericert-4b012187df7c66bef2300252058f27ac79337325.zip |
Rename lit directory
Diffstat (limited to 'src/hls/RTLBlockgen.v')
-rw-r--r-- | src/hls/RTLBlockgen.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/hls/RTLBlockgen.v b/src/hls/RTLBlockgen.v index 6d38e4f..beca0ea 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/basic-block-generation.org::rtlblockgen-imports][rtlblockgen-imports]] *) +(* [[file:../../docs/basic-block-generation.org::rtlblockgen-imports][rtlblockgen-imports]] *) Require compcert.backend.RTL. Require Import compcert.common.AST. Require Import compcert.lib.Maps. @@ -148,7 +148,7 @@ 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. -(* [[file:../../lit/basic-block-generation.org::rtlblockgen-main][rtlblockgen-main]] *) +(* [[file:../../docs/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 |