diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-09-05 13:12:17 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-09-05 13:12:17 +0200 |
| commit | effcbf7fab15673f10dfc2d455cb723b29515d5b (patch) | |
| tree | f635daff407a4f1b773cda33c4a0399a145ed5ac /lib/Coqlib.v | |
| parent | 64a1e734dfe24194bafd33cff1fbe4d9e1cfdf14 (diff) | |
| download | compcert-kvx-effcbf7fab15673f10dfc2d455cb723b29515d5b.tar.gz compcert-kvx-effcbf7fab15673f10dfc2d455cb723b29515d5b.zip | |
Removed some implict arguments.
Also changed Local Open to Open Local.
Diffstat (limited to 'lib/Coqlib.v')
| -rw-r--r-- | lib/Coqlib.v | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 6fa82492..18d4d7e1 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -1200,7 +1200,7 @@ Proof. subst; exists b1; auto. exploit IHlist_forall2; eauto. intros (x2 & U & V); exists x2; auto. Qed. - + Lemma list_forall2_in_right: forall x2 l1 l2, list_forall2 l1 l2 -> In x2 l2 -> exists x1, In x1 l1 /\ P x1 x2. @@ -1209,7 +1209,7 @@ Proof. subst; exists a1; auto. exploit IHlist_forall2; eauto. intros (x1 & U & V); exists x1; auto. Qed. - + End FORALL2. Lemma list_forall2_imply: @@ -1277,11 +1277,9 @@ Qed. (** * Definitions and theorems over boolean types *) -Definition proj_sumbool (P Q: Prop) (a: {P} + {Q}) : bool := +Definition proj_sumbool {P Q: Prop} (a: {P} + {Q}) : bool := if a then true else false. -Implicit Arguments proj_sumbool [P Q]. - Coercion proj_sumbool: sumbool >-> bool. Lemma proj_sumbool_true: |