fix compilation error after merge

REPROSEC · Oct 15, 2024 · 1cc79bf · 1cc79bf
1 parent 9d120da
commit 1cc79bf
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/src/core/DY.Core.Trace.Base.fst b/src/core/DY.Core.Trace.Base.fst
@@ -401,7 +401,7 @@ val get_event_at_trace_forget_labels:
   tr:trace -> i:timestamp{i < length tr} ->
   Lemma (
     length_trace_forget_labels tr;
-    get_event_at (trace_forget_labels tr) i == (fmap_trace_event (forget_label ()) (get_event_at tr i))
+    get_event_at (trace_forget_labels tr) i == (fmap_trace_event forget_label (get_event_at tr i))
   )
 let rec get_event_at_trace_forget_labels tr i =
   length_trace_forget_labels tr;
@@ -415,7 +415,7 @@ val event_at_trace_forget_labels:
   tr:trace -> i:timestamp -> ev:trace_event ->
   Lemma
   (requires event_at tr i ev)
-  (ensures event_at (trace_forget_labels tr) i (fmap_trace_event (forget_label ()) ev))
+  (ensures event_at (trace_forget_labels tr) i (fmap_trace_event forget_label ev))
 let event_at_trace_forget_labels tr i ev =
   length_trace_forget_labels tr;
   if i >= length tr then ()
@@ -427,10 +427,10 @@ val event_exists_trace_forget_labels:
   tr:trace -> ev:trace_event ->
   Lemma
   (requires event_exists tr ev)
-  (ensures event_exists (trace_forget_labels tr) (fmap_trace_event (forget_label ()) ev))
+  (ensures event_exists (trace_forget_labels tr) (fmap_trace_event forget_label ev))
 let event_exists_trace_forget_labels tr ev =
   eliminate exists i. event_at tr i ev
-  returns event_exists (trace_forget_labels tr) (fmap_trace_event (forget_label ()) ev)
+  returns event_exists (trace_forget_labels tr) (fmap_trace_event forget_label ev)
   with _. (
     event_at_trace_forget_labels tr i ev
   )