aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/Partition.ml
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2022-03-24 10:04:47 +0000
committerYann Herklotz <git@yannherklotz.com>2022-03-24 10:04:47 +0000
commit4b012187df7c66bef2300252058f27ac79337325 (patch)
treec9fa8c54725ab2126b59199a7718ff241b78121f /src/hls/Partition.ml
parent9eeb3845eb466189276fb16e08c41902b430c342 (diff)
downloadvericert-4b012187df7c66bef2300252058f27ac79337325.tar.gz
vericert-4b012187df7c66bef2300252058f27ac79337325.zip
Rename lit directory
Diffstat (limited to 'src/hls/Partition.ml')
-rw-r--r--src/hls/Partition.ml6
1 files changed, 4 insertions, 2 deletions
diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml
index d7972e5..545277b 100644
--- a/src/hls/Partition.ml
+++ b/src/hls/Partition.ml
@@ -1,6 +1,6 @@
- (*
+(*
* Vericert: Verified high-level synthesis.
- * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
+ * Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com>
*
* 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 <https://www.gnu.org/licenses/>.
*)
+(* [[file:../../docs/basic-block-generation.org::partition-main][partition-main]] *)
open Printf
open Clflags
open Camlcoq
@@ -122,3 +123,4 @@ let function_from_RTL f =
}
let partition = function_from_RTL
+(* partition-main ends here *)