diff options
| -rw-r--r-- | theories/FSets/FSetDecide.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v index 2769c76116..cc78fdb4da 100644 --- a/theories/FSets/FSetDecide.v +++ b/theories/FSets/FSetDecide.v @@ -416,7 +416,7 @@ the above form: propositions of interest. *) Inductive FSet_elt_Prop : Prop -> Prop := - | eq_Prop : forall (S : Set) (x y : S), + | eq_Prop : forall (S : Type) (x y : S), FSet_elt_Prop (x = y) | eq_elt_prop : forall x y, FSet_elt_Prop (E.eq x y) |