diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-05-26 10:39:25 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-05-26 10:39:25 +0200 |
| commit | bce2346a26f87e6fed7376d9d8c9050504d048ea (patch) | |
| tree | ec7b27c6e98ba173be5d73defbdb6332ec724f7c /src/State.v | |
| parent | 124c8919b833bf0c2c57751464712381d39b5bec (diff) | |
| download | smtcoq-bce2346a26f87e6fed7376d9d8c9050504d048ea.tar.gz smtcoq-bce2346a26f87e6fed7376d9d8c9050504d048ea.zip | |
Port the Coq part
Diffstat (limited to 'src/State.v')
| -rw-r--r-- | src/State.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/State.v b/src/State.v index 663b2b3..4431fbb 100644 --- a/src/State.v +++ b/src/State.v @@ -10,7 +10,7 @@ (**************************************************************************) -Require Import List Bool Int63 PArray Omega. +Require Import List Bool Int63 PArray Psatz. (* Require Import AxiomesInt. *) @@ -239,7 +239,7 @@ Proof. rewrite <- eqb_spec;trivial. rewrite <- not_true_iff_false in H, H0. unfold is_true in *;rewrite ltb_spec in H |- *;rewrite eqb_spec in H0. - assert ([|x|] <> [|y|]) by (intros Heq;apply H0, to_Z_inj;trivial);omega. + assert ([|x|] <> [|y|]) by (intros Heq;apply H0, to_Z_inj;trivial);lia. Qed. @@ -358,7 +358,7 @@ Module C. intros rho resolve_correct Hc1;simpl in Hc1. induction c2;simpl;try discriminate. generalize (compare_spec' l1 a);destruct (l1 ?= a);intros;subst;simpl. - simpl in Hc1;destruct (Lit.interp rho a);simpl in *;auto. + simpl in Hc1;destruct (Lit.interp rho l1);simpl in *;auto. generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a == 1);intros. rewrite or_correct. rewrite H1, Lit.interp_neg in Hc1;trivial;destruct (Lit.interp rho a). |