diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-08 21:00:28 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-08 21:00:28 +0100 |
| commit | 68baba2d3b8c5b72cebe598a406ef7b5646bcca3 (patch) | |
| tree | 8cfd7dc31012a751d58236e276ba321874090181 /lib | |
| parent | 1b6667cf268189104bc3320e83fa23fe0d053717 (diff) | |
| parent | 6ca9f9bfc7119f1ca4f48de3b5a37cbaee07e4fd (diff) | |
| download | compcert-kvx-68baba2d3b8c5b72cebe598a406ef7b5646bcca3.tar.gz compcert-kvx-68baba2d3b8c5b72cebe598a406ef7b5646bcca3.zip | |
Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-upstream-merge
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/BoolEqual.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/lib/BoolEqual.v b/lib/BoolEqual.v index c9e7bad5..e8c1d831 100644 --- a/lib/BoolEqual.v +++ b/lib/BoolEqual.v @@ -106,8 +106,8 @@ Ltac bool_eq_refl_case := end. Ltac bool_eq_refl := - let H := fresh "Hrec" in let x := fresh "x" in - fix H 1; intros x; destruct x; simpl; bool_eq_refl_case. + let Hrec := fresh "Hrec" in let x := fresh "x" in + fix Hrec 1; intros x; destruct x; simpl; bool_eq_refl_case. Lemma false_not_true: forall (P: Prop), false = true -> P. @@ -124,7 +124,6 @@ Qed. Ltac bool_eq_sound_case := match goal with - | [ H: false = true |- _ ] => exact (false_not_true _ H) | [ H: _ && _ = true |- _ ] => apply andb_prop in H; destruct H; bool_eq_sound_case | [ H: proj_sumbool ?a = true |- _ ] => apply proj_sumbool_true in H; bool_eq_sound_case | [ |- ?C ?x1 ?x2 ?x3 ?x4 = ?C ?y1 ?y2 ?y3 ?y4 ] => apply f_equal4; auto @@ -137,7 +136,9 @@ Ltac bool_eq_sound_case := Ltac bool_eq_sound := let Hrec := fresh "Hrec" in let x := fresh "x" in let y := fresh "y" in - fix Hrec 1; intros x y; destruct x, y; simpl; intro; bool_eq_sound_case. + let H := fresh "EQ" in + fix Hrec 1; intros x y; destruct x, y; intro H; + try (apply (false_not_true _ H)); simpl in H; bool_eq_sound_case. Lemma dec_eq_from_bool_eq: forall (A: Type) (f: A -> A -> bool) |