From 147b202286b1d48fda3bdcfec1ab4001e4880aac Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 12 Jan 2016 14:28:58 +0100
Subject: [PATCH] More consistent naming.
---
theories/fin_maps.v | 2 +-
theories/option.v | 4 ++--
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 791ef2d3..b51728b5 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1532,7 +1532,7 @@ Tactic Notation "simplify_map_equality" "by" tactic3(tac) :=
repeat match goal with
| _ => progress simpl_map by tac
| _ => progress simplify_equality
- | _ => progress simpl_option_monad by tac
+ | _ => progress simpl_option by tac
| H : {[ _ ↦ _ ]} !! _ = None |- _ => rewrite lookup_singleton_None in H
| H : {[ _ ↦ _ ]} !! _ = Some _ |- _ =>
rewrite lookup_singleton_Some in H; destruct H
diff --git a/theories/option.v b/theories/option.v
index 08bc2bc6..237194c2 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -261,7 +261,7 @@ Lemma option_guard_iff {A} P Q `{Decision P, Decision Q} (x : option A) :
(P ↔ Q) → guard P; x = guard Q; x.
Proof. intros [??]. repeat case_option_guard; intuition. Qed.
-Tactic Notation "simpl_option_monad" "by" tactic3(tac) :=
+Tactic Notation "simpl_option" "by" tactic3(tac) :=
let assert_Some_None A o H := first
[ let x := fresh in evar (x:A); let x' := eval unfold x in x in clear x;
assert (o = Some x') as H by tac
@@ -308,7 +308,7 @@ Tactic Notation "simpl_option_monad" "by" tactic3(tac) :=
Tactic Notation "simplify_option_equality" "by" tactic3(tac) :=
repeat match goal with
| _ => progress simplify_equality'
- | _ => progress simpl_option_monad by tac
+ | _ => progress simpl_option by tac
| _ : maybe _ ?x = Some _ |- _ => is_var x; destruct x
| _ : maybe2 _ ?x = Some _ |- _ => is_var x; destruct x
| _ : maybe3 _ ?x = Some _ |- _ => is_var x; destruct x
--
GitLab