diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2017-10-02 22:46:39 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2017-10-02 22:46:39 +0200 |
| commit | c41d405ee2c9e2ab070c69d91feb8441ab570590 (patch) | |
| tree | f51603cc3498cf137aaa8e0c623636cf3da960dd | |
| parent | 0a599dca5b7988ce5c28a641dfdfcca14ff18863 (diff) | |
| download | smtcoq-c41d405ee2c9e2ab070c69d91feb8441ab570590.tar.gz smtcoq-c41d405ee2c9e2ab070c69d91feb8441ab570590.zip | |
Towards Coq 8.6
| -rw-r--r-- | src/euf/Euf.v | 15 | ||||
| -rw-r--r-- | src/lia/Lia.v | 4 |
2 files changed, 9 insertions, 10 deletions
diff --git a/src/euf/Euf.v b/src/euf/Euf.v index 53e3ebe..70b23da 100644 --- a/src/euf/Euf.v +++ b/src/euf/Euf.v @@ -14,7 +14,6 @@ (**************************************************************************) -(* Add LoadPath ".." as SMTCoq. *) Require Import Bool List Int63 PArray. Require Import State SMT_terms. @@ -236,7 +235,7 @@ Section certif. match goal with | [ H1 : is_true (Typ.eqb ?a ?t1), H2 : is_true (Typ.eqb ?a ?t2) |- _ ] => - assert (W:= tunicity _ _ _ H1 H2);try subst + assert (W:= tunicity _ _ _ H1 H2) | _ => idtac end. @@ -290,11 +289,11 @@ Section certif. rewrite orb_true_iff, !andb_true_iff in H7;destruct H7 as [[H7 H8] | [H7 H8]]. rewrite eqb_spec in H7. rewrite eqb_spec in H8. subst. - tunicity. rewrite H4, H1;auto. + tunicity. subst t. rewrite H4, H1;auto. rewrite eqb_spec in H7. rewrite eqb_spec in H8. subst. - tunicity;rewrite interp_binop_eqb_sym in H1;rewrite H4, H1;auto. + tunicity;subst t;rewrite interp_binop_eqb_sym in H1;rewrite H4, H1;auto. apply get_eq_interp;intros. - destruct (Int63Properties.reflect_eqb t2 b);subst;tunicity. + destruct (Int63Properties.reflect_eqb t2 b). subst;tunicity; subst t. apply (IHeqs u);trivial. simpl;unfold is_true;rewrite orb_true_iff. rewrite Lit.interp_nlit;unfold Var.interp. @@ -303,7 +302,7 @@ Section certif. destruct H1;[left | auto]. apply interp_binop_eqb_trans with (4:= H1);trivial. rewrite interp_binop_eqb_sym;trivial. - destruct (Int63Properties.reflect_eqb t2 a0); subst;tunicity. + destruct (Int63Properties.reflect_eqb t2 a0); subst;tunicity; try subst t. apply (IHeqs u);trivial. simpl;unfold is_true;rewrite orb_true_iff. rewrite Lit.interp_nlit;unfold Var.interp. @@ -311,7 +310,7 @@ Section certif. case_eq (rho (Lit.blit a));[rewrite H4; intros | simpl;auto]. destruct H1;[left | auto]. apply interp_binop_eqb_trans with (4:= H1);trivial. - destruct (Int63Properties.reflect_eqb t1 b);subst;tunicity. + destruct (Int63Properties.reflect_eqb t1 b);subst;tunicity; try subst t. apply (IHeqs u);trivial. simpl;unfold is_true;rewrite orb_true_iff. rewrite Lit.interp_nlit;unfold Var.interp. @@ -319,7 +318,7 @@ Section certif. case_eq (rho (Lit.blit a));[rewrite H4; intros | simpl;auto]. destruct H1;[left | auto]. apply interp_binop_eqb_trans with (5:= H1);trivial. - destruct (Int63Properties.reflect_eqb t1 a0);[subst;tunicity|auto]. + destruct (Int63Properties.reflect_eqb t1 a0);[subst;tunicity; try subst t|auto]. apply (IHeqs u);trivial. simpl;unfold is_true;rewrite orb_true_iff. rewrite Lit.interp_nlit;unfold Var.interp. diff --git a/src/lia/Lia.v b/src/lia/Lia.v index 977612f..d8e89f3 100644 --- a/src/lia/Lia.v +++ b/src/lia/Lia.v @@ -1513,7 +1513,7 @@ Transparent build_z_atom. case_eq ((a0 == a1) && (a0 == b1) && (b == b0) && (b == a2)); intros; subst; try (unfold C.valid; apply valid_C_true; trivial). repeat(apply andb_prop in H19; destruct H19). - apply Int63Properties.eqb_spec in H19;apply Int63Properties.eqb_spec in H20;apply Int63Properties.eqb_spec in H21;apply Int63Properties.eqb_spec in H22;subst. + apply Int63Properties.eqb_spec in H19;apply Int63Properties.eqb_spec in H20;apply Int63Properties.eqb_spec in H21;apply Int63Properties.eqb_spec in H22; subst a0 b. unfold C.interp; simpl; rewrite orb_false_r. unfold Lit.interp; rewrite Lit.is_pos_lit. unfold Var.interp; rewrite Lit.blit_lit. @@ -1561,7 +1561,7 @@ Transparent build_z_atom. case_eq ((a0 == b0) && (a0 == a2) && (b == a1) && (b == b1)); intros; subst; try (unfold C.valid; apply valid_C_true; trivial). repeat(apply andb_prop in H19; destruct H19). - apply Int63Properties.eqb_spec in H19;apply Int63Properties.eqb_spec in H20;apply Int63Properties.eqb_spec in H21;apply Int63Properties.eqb_spec in H22;subst. + apply Int63Properties.eqb_spec in H19;apply Int63Properties.eqb_spec in H20;apply Int63Properties.eqb_spec in H21;apply Int63Properties.eqb_spec in H22;subst a0 b. unfold C.interp; simpl; rewrite orb_false_r. unfold Lit.interp; rewrite Lit.is_pos_lit. unfold Var.interp; rewrite Lit.blit_lit. |