diff options
Diffstat (limited to 'theories/micromega/Tauto.v')
| -rw-r--r-- | theories/micromega/Tauto.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/micromega/Tauto.v b/theories/micromega/Tauto.v index 515372466a..e4129f8382 100644 --- a/theories/micromega/Tauto.v +++ b/theories/micromega/Tauto.v @@ -1371,13 +1371,13 @@ Section S. destruct pol;auto. generalize (is_cnf_tt_inv (xcnf (negb true) f1)). destruct (is_cnf_tt (xcnf (negb true) f1)). - + intros. + + intros H. rewrite H by auto. reflexivity. + generalize (is_cnf_ff_inv (xcnf (negb true) f1)). destruct (is_cnf_ff (xcnf (negb true) f1)). - * intros. + * intros H. rewrite H by auto. unfold or_cnf_opt. simpl. |