Skip to content
Snippets Groups Projects
Commit b9c7af38 authored by Dan Frumin's avatar Dan Frumin Committed by Robbert Krebbers
Browse files

fix some tp_ tactics

parent 4ba6f5be
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/logic/proofmode/spec_tactics.v
+ 5
− 5
View file @ b9c7af38
...@@ -130,11 +130,11 @@ Tactic Notation "tp_rec" constr(j) := tp_pure j (App _ _). ...@@ -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_seq" constr(j) := tp_rec j.
Tactic Notation "tp_let" 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_lam" constr(j) := tp_rec j.
Tactic Notation "tp_fst" constr(j) := tp_pure j (Fst (Pair _ _)). Tactic Notation "tp_fst" constr(j) := tp_pure j (Fst (PairV _ _)).
Tactic Notation "tp_snd" constr(j) := tp_pure j (Snd (Pair _ _)). Tactic Notation "tp_snd" constr(j) := tp_pure j (Snd (PairV _ _)).
Tactic Notation "tp_proj" constr(j) := tp_pure j (_ (Pair _ _)). Tactic Notation "tp_proj" constr(j) := tp_pure j (_ (PairV _ _)).
Tactic Notation "tp_case_inl" constr(j) := tp_pure j (Case (InjL _) _ _). Tactic Notation "tp_case_inl" constr(j) := tp_pure j (Case (InjLV _) _ _).
Tactic Notation "tp_case_inr" constr(j) := tp_pure j (Case (InjR _) _ _). 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_case" constr(j) := tp_pure j (Case _ _ _).
Tactic Notation "tp_binop" constr(j) := tp_pure j (BinOp _ _ _). Tactic Notation "tp_binop" constr(j) := tp_pure j (BinOp _ _ _).
Tactic Notation "tp_op" constr(j) := tp_binop j. Tactic Notation "tp_op" constr(j) := tp_binop j.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment