diff options
-rw-r--r-- | backend/Deadcodeproof.v | 3 | ||||
-rw-r--r-- | backend/Inliningproof.v | 4 | ||||
-rw-r--r-- | backend/NeedDomain.v | 4 | ||||
-rw-r--r-- | backend/Unusedglobproof.v | 2 | ||||
-rw-r--r-- | cfrontend/Cexec.v | 12 | ||||
-rw-r--r-- | cfrontend/Ctypes.v | 4 | ||||
-rwxr-xr-x | configure | 8 | ||||
-rw-r--r-- | flocq/Appli/Fappli_IEEE.v | 1 | ||||
-rw-r--r-- | flocq/Core/Fcore_digits.v | 3 |
9 files changed, 22 insertions, 19 deletions
diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index 52f1f112..fa402e9f 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -978,7 +978,8 @@ Ltac UseTransfer := eapply match_succ_states; eauto. simpl; auto. destruct res; auto. apply eagree_set_undef; auto. eapply magree_storebytes_left; eauto. - exploit aaddr_arg_sound; eauto. + clear H3. + exploit aaddr_arg_sound; eauto. intros (bc & A & B & C). intros. eapply nlive_contains; eauto. erewrite Mem.loadbytes_length in H0 by eauto. diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index d06fa997..d5d7e033 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -1171,11 +1171,11 @@ Proof. rewrite <- SP in MS0. eapply match_stacks_invariant; eauto. intros. destruct (eq_block b1 stk). - subst b1. rewrite D in H8; inv H8. subst b2. eelim Plt_strict; eauto. + subst b1. rewrite D in H8; inv H8. eelim Plt_strict; eauto. rewrite E in H8; auto. intros. exploit Mem.perm_alloc_inv. eexact H. eauto. destruct (eq_block b1 stk); intros; auto. - subst b1. rewrite D in H8; inv H8. subst b2. eelim Plt_strict; eauto. + subst b1. rewrite D in H8; inv H8. eelim Plt_strict; eauto. intros. eapply Mem.perm_alloc_1; eauto. intros. exploit Mem.perm_alloc_inv. eexact A. eauto. rewrite dec_eq_false; auto. diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v index a53040f9..8e8b9c0b 100644 --- a/backend/NeedDomain.v +++ b/backend/NeedDomain.v @@ -1255,8 +1255,8 @@ Proof. split; simpl; auto; intros. rewrite PTree.gsspec in H6. destruct (peq id0 id). + inv H6. destruct H3. congruence. destruct gl!id as [iv0|] eqn:NG. - rewrite ISet.In_add. intros [P|P]. omega. eelim GL; eauto. - rewrite ISet.In_interval. omega. + unfold iv'; rewrite ISet.In_add. intros [P|P]. omega. eelim GL; eauto. + unfold iv'; rewrite ISet.In_interval. omega. + eauto. - (* Stk ofs *) split; simpl; auto; intros. destruct H3. diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index 7e9c3ca0..c79ae4fd 100644 --- a/backend/Unusedglobproof.v +++ b/backend/Unusedglobproof.v @@ -1015,7 +1015,7 @@ Proof. { rewrite STK, TSTK. apply match_stacks_incr with j; auto. intros. destruct (eq_block b1 stk). - subst b1. rewrite F in H1; inv H1. subst b2. split; apply Ple_refl. + subst b1. rewrite F in H1; inv H1. split; apply Ple_refl. rewrite G in H1 by auto. congruence. } econstructor; split. eapply exec_function_internal; eauto. diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 4dcf2a47..a9ffcd3d 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -130,8 +130,8 @@ Definition val_of_eventval (ev: eventval) (t: typ) : option val := Ltac mydestr := match goal with - | [ |- None = Some _ -> _ ] => intro X; discriminate - | [ |- Some _ = Some _ -> _ ] => intro X; inv X + | [ |- None = Some _ -> _ ] => let X := fresh "X" in intro X; discriminate + | [ |- Some _ = Some _ -> _ ] => let X := fresh "X" in intro X; inv X | [ |- match ?x with Some _ => _ | None => _ end = Some _ -> _ ] => destruct x eqn:?; mydestr | [ |- match ?x with true => _ | false => _ end = Some _ -> _ ] => destruct x eqn:?; mydestr | [ |- match ?x with left _ => _ | right _ => _ end = Some _ -> _ ] => destruct x; mydestr @@ -2038,12 +2038,14 @@ Definition do_step (w: world) (s: state) : list transition := Ltac myinv := match goal with - | [ |- In _ nil -> _ ] => intro X; elim X + | [ |- In _ nil -> _ ] => let X := fresh "X" in intro X; elim X | [ |- In _ (ret _ _) -> _ ] => + let X := fresh "X" in intro X; elim X; clear X; - [intro EQ; unfold ret in EQ; inv EQ; myinv | myinv] + [let EQ := fresh "EQ" in intro EQ; unfold ret in EQ; inv EQ; myinv | myinv] | [ |- In _ (_ :: nil) -> _ ] => - intro X; elim X; clear X; [intro EQ; inv EQ; myinv | myinv] + let X := fresh "X" in + intro X; elim X; clear X; [let EQ := fresh "EQ" in intro EQ; inv EQ; myinv | myinv] | [ |- In _ (match ?x with Some _ => _ | None => _ end) -> _ ] => destruct x eqn:?; myinv | [ |- In _ (match ?x with false => _ | true => _ end) -> _ ] => destruct x eqn:?; myinv | [ |- In _ (match ?x with left _ => _ | right _ => _ end) -> _ ] => destruct x; myinv diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index 0794743d..8d6cdb24 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -1064,7 +1064,7 @@ Proof. destruct (complete_members env m) eqn:C; simplify_eq EQ. clear EQ; intros EQ. rewrite PTree.gsspec. intros [A|A]; auto. destruct (peq id id0); auto. - inv A. rewrite <- H1; auto. + inv A. rewrite <- H0; auto. } intros. exploit REC; eauto. rewrite PTree.gempty. intuition congruence. Qed. @@ -1519,7 +1519,7 @@ Local Transparent Linker_program. - intros. exploit link_match_fundef; eauto. intros (tf & A & B). exists tf; auto. - intros. Local Transparent Linker_types. - simpl in *. destruct (type_eq v1 v2); inv H4. subst v tv2. exists tv1; rewrite dec_eq_true; auto. + simpl in *. destruct (type_eq v1 v2); inv H4. exists v; rewrite dec_eq_true; auto. - eauto. - eauto. - eauto. @@ -407,15 +407,15 @@ missingtools=false echo "Testing Coq... " | tr -d '\n' coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p') case "$coq_ver" in - 8.5pl2|8.5pl3) + 8.6) echo "version $coq_ver -- good!";; ?.*) echo "version $coq_ver -- UNSUPPORTED" - echo "Error: CompCert requires Coq version 8.5pl2." + echo "Error: CompCert requires Coq version 8.6." missingtools=true;; *) echo "NOT FOUND" - echo "Error: make sure Coq version 8.5pl2 is installed." + echo "Error: make sure Coq version 8.6 is installed." missingtools=true;; esac @@ -448,7 +448,7 @@ else ocaml_opt_comp=false fi -MENHIR_REQUIRED=20160303 +MENHIR_REQUIRED=20161201 echo "Testing Menhir... " | tr -d '\n' menhir_ver=`menhir --version 2>/dev/null | sed -n -e 's/^.*version \([0-9]*\).*$/\1/p'` case "$menhir_ver" in diff --git a/flocq/Appli/Fappli_IEEE.v b/flocq/Appli/Fappli_IEEE.v index 23999a50..a4accfa5 100644 --- a/flocq/Appli/Fappli_IEEE.v +++ b/flocq/Appli/Fappli_IEEE.v @@ -1,3 +1,4 @@ +Unset Bracketing Last Introduction Pattern. (** This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ diff --git a/flocq/Core/Fcore_digits.v b/flocq/Core/Fcore_digits.v index d40c1a09..7d1d490a 100644 --- a/flocq/Core/Fcore_digits.v +++ b/flocq/Core/Fcore_digits.v @@ -853,8 +853,7 @@ Proof. intros n Zn. rewrite <- (Zdigits_abs n). assert (Hn: (0 < Zabs n)%Z). -destruct n ; try easy. -now elim Zn. +destruct n ; now easy. destruct (Zabs n) as [|p|p] ; try easy ; clear. simpl. generalize 1%Z (radix_val beta) (refl_equal Lt : (0 < 1)%Z). |