aboutsummaryrefslogtreecommitdiffstats
path: root/src/SoftwarePipelining/SPTyping.mli
blob: c231ddd96fc03f17d93e4d9c8d837cc621da4195 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
(***********************************************************************)
(*                                                                     *)
(*                        Compcert Extensions                          *)
(*                                                                     *)
(*                       Jean-Baptiste Tristan                         *)
(*                                                                     *)
(*  All rights reserved.  This file is distributed under the terms     *)
(*  described in file ../../LICENSE.                                   *)
(*                                                                     *)
(***********************************************************************)



val type_function : RTL.coq_function -> unit