diff --git a/compiler/src/compiler/Pipeline.v b/compiler/src/compiler/Pipeline.v index c890774d0..a725163b9 100644 --- a/compiler/src/compiler/Pipeline.v +++ b/compiler/src/compiler/Pipeline.v @@ -66,9 +66,9 @@ Section WithWordAndMem. Record Lang := { Program: Type; - Valid: Program -> Prop; - Leakage: Type; - Call(pick_sp: list Leakage -> word)(p: Program)(funcname: string) + Valid: Program -> Prop; + Leakage: Type; + Call(p: Program)(funcname: string)(pick_sp: list Leakage -> word) (k: list Leakage)(t: trace)(m: mem)(argvals: list word)(mc: MetricLog) (post: list Leakage -> trace -> mem -> list word -> MetricLog -> Prop): Prop; }.