diff --git a/theories/logic/proofmode/spec_tactics.v b/theories/logic/proofmode/spec_tactics.v
index 4f08c9864dc5fa24f9d84f5bdedd21a359e8bb2c..3ebd7e4b6c7bee518f40a73f7ae7d581ef93a5fd 100644
--- a/theories/logic/proofmode/spec_tactics.v
+++ b/theories/logic/proofmode/spec_tactics.v
@@ -130,11 +130,11 @@ Tactic Notation "tp_rec" constr(j) := tp_pure j (App _ _).
 Tactic Notation "tp_seq" constr(j) := tp_rec j.
 Tactic Notation "tp_let" constr(j) := tp_rec j.
 Tactic Notation "tp_lam" constr(j) := tp_rec j.
-Tactic Notation "tp_fst" constr(j) := tp_pure j (Fst (Pair _ _)).
-Tactic Notation "tp_snd" constr(j) := tp_pure j (Snd (Pair _ _)).
-Tactic Notation "tp_proj" constr(j) := tp_pure j (_ (Pair _ _)).
-Tactic Notation "tp_case_inl" constr(j) := tp_pure j (Case (InjL _) _ _).
-Tactic Notation "tp_case_inr" constr(j) := tp_pure j (Case (InjR _) _ _).
+Tactic Notation "tp_fst" constr(j) := tp_pure j (Fst (PairV _ _)).
+Tactic Notation "tp_snd" constr(j) := tp_pure j (Snd (PairV _ _)).
+Tactic Notation "tp_proj" constr(j) := tp_pure j (_ (PairV _ _)).
+Tactic Notation "tp_case_inl" constr(j) := tp_pure j (Case (InjLV _) _ _).
+Tactic Notation "tp_case_inr" constr(j) := tp_pure j (Case (InjRV _) _ _).
 Tactic Notation "tp_case" constr(j) := tp_pure j (Case _ _ _).
 Tactic Notation "tp_binop" constr(j) := tp_pure j (BinOp _ _ _).
 Tactic Notation "tp_op" constr(j) := tp_binop j.