Fixed a few things that break after the removal of explicit module

identifiers, adding a "float_fabs" binding for the absolute
value function on floating-point numbers.

Fixed a long-standing problem in the Mizarlight Makefile by using
ocamlfind to find camlp5 - this in turn can be installed in an Opam
setting by "opam install ocamlfind", and is anyway already used in
the main "hol.ml" root file for recent OCamls.

Formal_ineqs/informal/informal_exp.hl

@@ -130,7 +130,7 @@ let exp_high_raw pp x =
       exp_neg_high_raw pp (abs_float x);;
 
 let reduce_float x =
-  let f = abs_float (float_of_ifloat x) in
+  let f = float_fabs (float_of_ifloat x) in
     if f <= exp_max_x then
       false, 0
     else

Jordan/float.ml

@@ -1136,7 +1136,7 @@ let (round_outward_float: int -> float -> Num.num) =
  fun  bprec f ->
   if (f=0.0) then (num 0) else
   begin
-    let b = abs_float f in
+    let b = float_fabs f in
     let sign = if (f >= 0.0) then I else minus_num in
     let (x,n) = frexp b in
     let u = int_of_float( ceil (ldexp x bprec)) in
@@ -1149,7 +1149,7 @@ let (round_inward_float: int -> float -> Num.num) =
   begin
     (* avoid overflow on 30 bit integers *)
     let bprec = if (bprec > 25) then 25 else bprec in
-    let b = abs_float f in
+    let b = float_fabs f in
     let sign = if (f >= 0.0) then I else minus_num in
     let (x,n) = frexp b in
     let u = int_of_float( floor (ldexp x bprec)) in

Mizarlight/Makefile

@@ -6,7 +6,7 @@
 
 pa_f.cmo: pa_f.ml; if test `ocamlc -version | cut -c1-3` = "3.0" ; \
                    then ocamlc -c -pp "camlp4r pa_extend.cmo q_MLast.cmo" -I +camlp4 pa_f.ml; \
-                   else ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" -I +camlp5 pa_f.ml; \
+                   else ocamlfind ocamlc -package camlp5 -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" -I +camlp5 pa_f.ml; \
                    fi
 
 clean:; rm -f pa_f.cmi pa_f.cmo

hol.ml

@@ -103,12 +103,16 @@ then loads "bignum_zarith.ml"
 else loads "bignum_num.ml";;
 
 (* ------------------------------------------------------------------------- *)
-(* Bind this to a name that is independent of OCaml versions before it       *)
-(* is potentially overwritten by a theorem of the same name. On older        *)
-(* OCaml versions it is "Pervasives.sqrt", and on newer ones "Float.sqrt".   *)
+(* Bind these to names that are independent of OCaml versions before they    *)
+(* are potentially overwritten by an identifier of the same name. In older   *)
+(* and newer Ocaml versions these are respectively:                          *)
+(*                                                                           *)
+(* Pervasives.sqrt -> Float.sqrt                                             *)
+(* Pervasives.abs_float -> Stdlib.abs_float / Float.abs                      *)
 (* ------------------------------------------------------------------------- *)
 
 let float_sqrt = sqrt;;
+let float_fabs = abs_float;;
 
 (* ------------------------------------------------------------------------- *)
 (* Various tweaks to OCaml and general library functions.                    *)