diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2019-11-14 20:30:48 +0100 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2019-11-14 20:30:48 +0100 |
| commit | 06bd8685c7dd00fbfe544615ca4d5e2f71cfaaed (patch) | |
| tree | 89073955579791e10910a7bdd89799aec47ec1d7 | |
| parent | 4294883295f02122cde3e43f73e166f40390520b (diff) | |
| download | smtcoq-06bd8685c7dd00fbfe544615ca4d5e2f71cfaaed.tar.gz smtcoq-06bd8685c7dd00fbfe544615ca4d5e2f71cfaaed.zip | |
Changing notation for implb (closes #51)
| -rw-r--r-- | examples/Example.v | 6 | ||||
| -rw-r--r-- | src/BoolToProp.v | 12 |
2 files changed, 9 insertions, 9 deletions
diff --git a/examples/Example.v b/examples/Example.v index 5bb1a83..04f82a7 100644 --- a/examples/Example.v +++ b/examples/Example.v @@ -11,7 +11,7 @@ (* [Require Import SMTCoq.SMTCoq.] loads the SMTCoq library. - If you are using native-coq instead of Coq 8.6, replace it with: + If you are using native-coq instead of Coq 8.9, replace it with: Require Import SMTCoq. *) @@ -389,11 +389,11 @@ Section CompCert. Hypothesis alloc_valid_block_1: forall m lo hi b, - valid_block (alloc_mem m lo hi) b --> ((b =? (alloc_block m lo hi)) || valid_block m b). + valid_block (alloc_mem m lo hi) b ---> ((b =? (alloc_block m lo hi)) || valid_block m b). Hypothesis alloc_valid_block_2: forall m lo hi b, - ((b =? (alloc_block m lo hi)) || valid_block m b) --> valid_block (alloc_mem m lo hi) b. + ((b =? (alloc_block m lo hi)) || valid_block m b) ---> valid_block (alloc_mem m lo hi) b. Hypothesis alloc_not_valid_block: forall m lo hi, diff --git a/src/BoolToProp.v b/src/BoolToProp.v index 1b8c923..8a3b134 100644 --- a/src/BoolToProp.v +++ b/src/BoolToProp.v @@ -16,8 +16,8 @@ Import BVList.BITVECTOR_LIST. Local Coercion is_true : bool >-> Sortclass. -Infix "-->" := implb (at level 60, right associativity) : bool_scope. -Infix "<-->" := Bool.eqb (at level 60, right associativity) : bool_scope. +Infix "--->" := implb (at level 60, right associativity) : bool_scope. +Infix "<--->" := Bool.eqb (at level 60, right associativity) : bool_scope. Ltac bool2prop := repeat @@ -43,8 +43,8 @@ Ltac bool2prop := | [ |- context[ Z.geb _ _ ] ] => unfold is_true; rewrite Z.geb_le | [ |- context[ Z.eqb _ _ ] ] => unfold is_true; rewrite Z.eqb_eq - | [ |- context[?G0 --> ?G1 ] ] => - unfold is_true; rewrite <- (@reflect_iff (G0 = true -> G1 = true) (G0 --> G1)); + | [ |- context[?G0 ---> ?G1 ] ] => + unfold is_true; rewrite <- (@reflect_iff (G0 = true -> G1 = true) (G0 ---> G1)); [ | apply implyP] | [ |- context[?G0 || ?G1 ] ] => @@ -55,8 +55,8 @@ Ltac bool2prop := unfold is_true; rewrite <- (@reflect_iff (G0 = true /\ G1 = true) (G0 && G1)); [ | apply andP] - | [ |- context[?G0 <--> ?G1 ] ] => - unfold is_true; rewrite <- (@reflect_iff (G0 = true <-> G1 = true) (G0 <--> G1)); + | [ |- context[?G0 <---> ?G1 ] ] => + unfold is_true; rewrite <- (@reflect_iff (G0 = true <-> G1 = true) (G0 <---> G1)); [ | apply iffP] | [ |- context[ negb ?G ] ] => |