diff options
Diffstat (limited to 'powerpc/SelectOpproof.v')
| -rw-r--r-- | powerpc/SelectOpproof.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 3e34244d..63066135 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -1062,7 +1062,6 @@ Proof. - constructor; auto. Qed. -<<<<<<< HEAD (* floating-point division without HELPERS *) Theorem eval_divf_base: forall le a b x y, @@ -1083,7 +1082,7 @@ Proof. intros; unfold divfs_base. TrivialExists. Qed. -======= + (** Platform-specific known builtins *) Theorem eval_platform_builtin: |