diff options
Diffstat (limited to 'otherlibs/num/arith_flags.mli')
| -rw-r--r-- | otherlibs/num/arith_flags.mli | 20 |
1 files changed, 0 insertions, 20 deletions
diff --git a/otherlibs/num/arith_flags.mli b/otherlibs/num/arith_flags.mli deleted file mode 100644 index 7dd6bc79d0..0000000000 --- a/otherlibs/num/arith_flags.mli +++ /dev/null @@ -1,20 +0,0 @@ -(**************************************************************************) -(* *) -(* OCaml *) -(* *) -(* Valerie Menissier-Morain, projet Cristal, INRIA Rocquencourt *) -(* *) -(* Copyright 1996 Institut National de Recherche en Informatique et *) -(* en Automatique. *) -(* *) -(* All rights reserved. This file is distributed under the terms of *) -(* the GNU Lesser General Public License version 2.1, with the *) -(* special exception on linking described in the file LICENSE. *) -(* *) -(**************************************************************************) - -val error_when_null_denominator_flag : bool ref -val normalize_ratio_flag : bool ref -val normalize_ratio_when_printing_flag : bool ref -val floating_precision : int ref -val approx_printing_flag : bool ref |