Commit a651a78a authored by François Bobot's avatar François Bobot
Browse files

readd jbuild file removed

parent 1943455e
(**************************************************************************)
(* This file is part of the extraction of the Flocq formalization of *)
(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *)
(* *)
(* Copyright (C) 2010-2013 Sylvie Boldo *)
(* *)
(* Copyright (C) 2010-2013 Guillaume Melquiond *)
(* *)
(* This library is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Lesser General Public *)
(* License as published by the Free Software Foundation; either *)
(* version 3 of the License, or (at your option) any later version. *)
(* *)
(* This library is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* COPYING file for more details. *)
(**************************************************************************)
open Farith_BinPos
(** val shift_pos :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int **)
let shift_pos n z =
Pos.iter (fun x -> Farith_Big.double x) z n
(**************************************************************************)
(* This file is part of the extraction of the Flocq formalization of *)
(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *)
(* *)
(* Copyright (C) 2010-2013 Sylvie Boldo *)
(* *)
(* Copyright (C) 2010-2013 Guillaume Melquiond *)
(* *)
(* This library is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Lesser General Public *)
(* License as published by the Free Software Foundation; either *)
(* version 3 of the License, or (at your option) any later version. *)
(* *)
(* This library is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* COPYING file for more details. *)
(**************************************************************************)
open Farith_BinPos
val shift_pos :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int
(library (
(name farith_extracted)
(libraries (zarith farith_big))
(wrapped false)
))
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment