diff options
Diffstat (limited to 'unit-tests/Tests_lfsc_tactics.v')
| -rw-r--r-- | unit-tests/Tests_lfsc_tactics.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/unit-tests/Tests_lfsc_tactics.v b/unit-tests/Tests_lfsc_tactics.v index a948e06..eb9744b 100644 --- a/unit-tests/Tests_lfsc_tactics.v +++ b/unit-tests/Tests_lfsc_tactics.v @@ -764,11 +764,11 @@ Section Group. Lemma simplification_right x1 x2 y: op x1 y ==? op x2 y -> x1 ==? x2. - Proof. intro H. smt_no_check H inverse'. Qed. + Proof. intro H. smt_no_check (H, inverse'). Qed. Lemma simplification_left x1 x2 y: op y x1 ==? op y x2 -> x1 ==? x2. - Proof. intro H. smt_no_check H inverse'. Qed. + Proof. intro H. smt_no_check (H, inverse'). Qed. Clear_lemmas. End Group. |