From 8831cde8ac53d47af1f5bd49c3df0e0b738fc618 Mon Sep 17 00:00:00 2001 From: Dan Frumin <dfrumin@cs.ru.nl> Date: Tue, 2 Jul 2019 12:46:46 +0200 Subject: [PATCH] fix some tp_ tactics --- theories/logic/proofmode/spec_tactics.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/theories/logic/proofmode/spec_tactics.v b/theories/logic/proofmode/spec_tactics.v index 4f08c98..3ebd7e4 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. -- GitLab