(* *********************************************************************) (* *) (* The Compcert verified compiler *) (* *) (* Xavier Leroy, INRIA Paris *) (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) (* under the terms of the INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) (** Instruction selection for 64-bit integer operations *) Require Import Coqlib. Require Import Compopts. Require Import AST Integers Floats. Require Import Op CminorSel. Require Import OpHelpers SelectOp SplitLong. (** This file is empty because we use the default implementation provided in [SplitLong]. *)