From c41d405ee2c9e2ab070c69d91feb8441ab570590 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Mon, 2 Oct 2017 22:46:39 +0200 Subject: Towards Coq 8.6 --- src/euf/Euf.v | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) (limited to 'src/euf/Euf.v') 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. -- cgit