diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-03-22 16:42:39 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-03-22 16:42:39 +0000 |
| commit | 5bb3e077854e33a7bd51d38f97970b08da171130 (patch) | |
| tree | c919d0208d0e1bd5464679748ef68e25ba2f902c /src/hls/Sat.v | |
| parent | 125348f2a99c947b1a141866e0e8f33f33d7134a (diff) | |
| download | vericert-5bb3e077854e33a7bd51d38f97970b08da171130.tar.gz vericert-5bb3e077854e33a7bd51d38f97970b08da171130.zip | |
Fix proofs in Sat.v
Diffstat (limited to 'src/hls/Sat.v')
| -rw-r--r-- | src/hls/Sat.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/Sat.v b/src/hls/Sat.v index b7596f6..428c176 100644 --- a/src/hls/Sat.v +++ b/src/hls/Sat.v @@ -119,7 +119,6 @@ Lemma satLit_contra : forall s l a cl, -> satClause cl a. unfold satLit, upd; simpl; intros. destruct (eq_nat_dec (snd l) (snd l)); intuition. - assert False; intuition. Qed. #[local] Hint Resolve satLit_contra : core. @@ -287,6 +286,7 @@ Lemma unitClauseTrue : forall l a fm, induction fm; intuition. inversion H. inversion H; subst; simpl in H0; intuition. + apply IHfm; eauto. inv H0. eauto. Qed. #[local] Hint Resolve unitClauseTrue : core. |