Skip to content

Commit 0139869

Browse files
committed
Fixing the marker link
1 parent 8f30948 commit 0139869

File tree

1 file changed

+5
-2
lines changed

1 file changed

+5
-2
lines changed

CoqOfRust/core/links/marker.v

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -25,12 +25,15 @@ Module PointeeSized.
2525
Definition trait (Self : Set) `{Link Self} : TraitMethod.Header.t :=
2626
("pinocchio::pointee::PointeeSized", [], [], Φ Self).
2727

28-
Class Run (Self : Set) `{Link Self} : Set := {}.
28+
Class Run (Self : Set) `{Link Self} : Set := {
29+
dummy_empty_class : unit;
30+
}.
2931
End PointeeSized.
3032

3133
(*
3234
pub struct PhantomData<T: PointeeSized>;
3335
*)
3436
Module PhantomData.
35-
Record t (T : Set) `{PointeeSized.Run T} : Set := {}.
37+
Inductive t (T : Set) `{PointeeSized.Run T} : Set :=
38+
| Make.
3639
End PhantomData.

0 commit comments

Comments
 (0)