From f05378e111181daa96ffa921001a85bbad8185b3 Mon Sep 17 00:00:00 2001 From: Peng Wang Date: Mon, 22 Feb 2016 17:53:31 -0500 Subject: [PATCH] Tweaked Ltac singletoner to display state space exploration in real time --- Frap.v | 3 ++- ModelChecking.v | 4 +++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/Frap.v b/Frap.v index b50e9d5..cfdfc38 100644 --- a/Frap.v +++ b/Frap.v @@ -104,7 +104,8 @@ Ltac model_check_done := Ltac singletoner := repeat match goal with - | _ => apply singleton_in + (* | _ => apply singleton_in *) + | [ |- _ ?S ] => idtac S; apply singleton_in | [ |- (_ \cup _) _ ] => apply singleton_in_other end. diff --git a/ModelChecking.v b/ModelChecking.v index 04892cc..9ab1515 100644 --- a/ModelChecking.v +++ b/ModelChecking.v @@ -302,7 +302,8 @@ Qed. Ltac singletoner := repeat match goal with - | _ => apply singleton_in + (* | _ => apply singleton_in *) + | [ |- _ ?S ] => idtac S; apply singleton_in | [ |- (_ \cup _) _ ] => apply singleton_in_other end. @@ -1572,3 +1573,4 @@ Theorem twoadd6_ok : Proof. twoadd. Qed. +