From 6ca015ff37524feedb2b9895a2098fc383faf5a5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 29 Jan 2017 21:12:09 +0100
Subject: [PATCH] Simplify introduction pattern parser.
---
theories/proofmode/intro_patterns.v | 14 +++++++-------
theories/proofmode/tactics.v | 9 ++-------
2 files changed, 9 insertions(+), 14 deletions(-)
diff --git a/theories/proofmode/intro_patterns.v b/theories/proofmode/intro_patterns.v
index 3f7f1b5ec..eb1ffdcff 100644
--- a/theories/proofmode/intro_patterns.v
+++ b/theories/proofmode/intro_patterns.v
@@ -16,7 +16,8 @@ Inductive intro_pat :=
| ISimpl : intro_pat
| IForall : intro_pat
| IAll : intro_pat
- | IClear : list (bool * string) → intro_pat. (* true = frame, false = clear *)
+ | IClear : string → intro_pat
+ | IClearFrame : string → intro_pat.
Module intro_pat.
Inductive token :=
@@ -140,15 +141,14 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
| TSimpl :: ts => parse_go ts (SPat ISimpl :: k)
| TAll :: ts => parse_go ts (SPat IAll :: k)
| TForall :: ts => parse_go ts (SPat IForall :: k)
- | TClearL :: ts => parse_clear ts [] k
+ | TClearL :: ts => parse_clear ts k
| _ => None
end
-with parse_clear (ts : list token)
- (ss : list (bool * string)) (k : stack) : option stack :=
+with parse_clear (ts : list token) (k : stack) : option stack :=
match ts with
- | TFrame :: TName s :: ts => parse_clear ts ((true,s) :: ss) k
- | TName s :: ts => parse_clear ts ((false,s) :: ss) k
- | TClearR :: ts => parse_go ts (SPat (IClear (reverse ss)) :: k)
+ | TFrame :: TName s :: ts => parse_clear ts (SPat (IClearFrame s) :: k)
+ | TName s :: ts => parse_clear ts (SPat (IClear s) :: k)
+ | TClearR :: ts => parse_go ts k
| _ => None
end.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 8b0486b28..d56432016 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -780,13 +780,8 @@ Tactic Notation "iIntros" constr(pat) :=
| ISimpl :: ?pats => simpl; go pats
| IForall :: ?pats => repeat iIntroForall; go pats
| IAll :: ?pats => repeat (iIntroForall || iIntro); go pats
- | IClear ?cpats :: ?pats =>
- let rec clr cpats :=
- match cpats with
- | [] => go pats
- | (false,?H) :: ?cpats => iClear H; clr cpats
- | (true,?H) :: ?cpats => iFrame H; clr cpats
- end in clr cpats
+ | IClear ?H :: ?pats => iClear H; go pats
+ | IClearFrame ?H :: ?pats => iFrame H; go pats
| IAlwaysElim ?pat :: ?pats =>
let H := iFresh in iIntro #H; iDestructHyp H as pat; go pats
| ?pat :: ?pats =>
--
GitLab