diff --git a/tests/gmap.v b/tests/gmap.v index 8fdc617474e441e0b5951c6a9a90bf2e7b725711..6cb7029b63ea9553c3255497fe63bd09b68fb38d 100644 --- a/tests/gmap.v +++ b/tests/gmap.v @@ -22,14 +22,14 @@ Proof. Show. Abort. -Goal 1 ∈ dom (M := gmap _ _) (gset _) (<[ 1 := 2 ]> ∅). +Goal 1 ∈ dom (M := gmap nat nat) (gset nat) (<[ 1 := 2 ]> ∅). Proof. Fail progress simpl. Fail progress cbn. Show. Abort. -Goal bool_decide (∅ =@{gset _} {[ 1; 2; 3 ]}) = false. +Goal bool_decide (∅ =@{gset nat} {[ 1; 2; 3 ]}) = false. Proof. Fail progress simpl. Fail progress cbn. @@ -37,7 +37,7 @@ Proof. reflexivity. Qed. -Goal bool_decide (∅ ≡@{gset _} {[ 1; 2; 3 ]}) = false. +Goal bool_decide (∅ ≡@{gset nat} {[ 1; 2; 3 ]}) = false. Proof. Fail progress simpl. Fail progress cbn. @@ -45,7 +45,7 @@ Proof. reflexivity. Qed. -Goal bool_decide (1 ∈@{gset _} {[ 1; 2; 3 ]}) = true. +Goal bool_decide (1 ∈@{gset nat} {[ 1; 2; 3 ]}) = true. Proof. Fail progress simpl. Fail progress cbn. @@ -53,7 +53,7 @@ Proof. reflexivity. Qed. -Goal bool_decide (∅ ##@{gset _} {[ 1; 2; 3 ]}) = true. +Goal bool_decide (∅ ##@{gset nat} {[ 1; 2; 3 ]}) = true. Proof. Fail progress simpl. Fail progress cbn. @@ -61,7 +61,7 @@ Proof. reflexivity. Qed. -Goal bool_decide (∅ ⊆@{gset _} {[ 1; 2; 3 ]}) = true. +Goal bool_decide (∅ ⊆@{gset nat} {[ 1; 2; 3 ]}) = true. Proof. Fail progress simpl. Fail progress cbn.