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 /src/euf/Euf.v | |
| parent | 0a599dca5b7988ce5c28a641dfdfcca14ff18863 (diff) | |
| download | smtcoq-c41d405ee2c9e2ab070c69d91feb8441ab570590.tar.gz smtcoq-c41d405ee2c9e2ab070c69d91feb8441ab570590.zip | |
Towards Coq 8.6
Diffstat (limited to 'src/euf/Euf.v')
| -rw-r--r-- | src/euf/Euf.v | 15 |
1 files changed, 7 insertions, 8 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. |