From 3ae53273148156f92e5ea233dfd11f7ee6d7fd4c Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 9 Feb 2016 13:11:58 -0500 Subject: [PATCH] Booleans and [propositional] --- Frap.v | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Frap.v b/Frap.v index 333720d..94e7211 100644 --- a/Frap.v +++ b/Frap.v @@ -1,5 +1,5 @@ -Require Import String Arith Omega Program Sets Relations Map Var Invariant. -Export String Arith Sets Relations Map Var Invariant. +Require Import String Arith Omega Program Sets Relations Map Var Invariant Bool. +Export String Arith Sets Relations Map Var Invariant Bool. Require Import List. Export List ListNotations. Open Scope string_scope. @@ -44,6 +44,7 @@ Ltac invert1 e := invert0 e || (invert e; []). Ltac invert2 e := invert1 e || (invert e; [|]). Ltac simplify := repeat progress (simpl in *; intros; try autorewrite with core in *). +Ltac propositional := intuition idtac. Ltac linear_arithmetic := intros; repeat match goal with