Skip to content
GitLab
Commit 28dcb4a3 authored by Dan Frumin's avatar Dan Frumin
Browse files

Fix a typo

parent 2505d0f6
Hide whitespace changes
Inline Side-by-side
theories/logrel/proofmode/tactics_rel.v
View file @ 28dcb4a3
......@@ -202,7 +202,7 @@ Tactic Notation "rel_pure_r" open_constr(ef) :=
Tactic Notation "rel_rec_r" := rel_pure_r (App (Rec _ _ _) _) || rel_pure_r (App _ _).
Tactic Notation "rel_seq_r" := rel_rec_r.
Tactic Notation "rel_ret_r" := rel_rec_r.
Tactic Notation "rel_let_r" := rel_rec_r.
Tactic Notation "rel_fst_r" := rel_pure_r (Fst (Pair _ _)).
Tactic Notation "rel_snd_r" := rel_pure_r (Snd (Pair _ _)).
Tactic Notation "rel_proj_r" := rel_pure_r (_ (Pair _ _)).
......
Supports Markdown
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