1
|
open Format
|
2
|
open LustreSpec
|
3
|
open Machine_code
|
4
|
open C_backend_common
|
5
|
open Utils
|
6
|
|
7
|
module type MODIFIERS_COQ =
|
8
|
sig
|
9
|
val pp_coq : bool -> formatter -> Machine_code.machine_t -> unit
|
10
|
end
|
11
|
|
12
|
module EmptyMod =
|
13
|
struct
|
14
|
let pp_coq x fmt m = ()
|
15
|
end
|
16
|
|
17
|
module Main = functor (Mod: MODIFIERS_COQ) ->
|
18
|
struct
|
19
|
let print_lib_coq fmt basename prog machines =
|
20
|
List.iter (Mod.pp_coq false fmt) machines;
|
21
|
end
|
22
|
|
23
|
(* Local Variables: *)
|
24
|
(* compile-command:"make -C ../../.." *)
|
25
|
(* End: *)
|