Merge branch 'master' into cleanup

1 files changed, 8 insertions, 8 deletions

diff --git a/driver/Interp.ml b/driver/Interp.ml
index e3a7d3b8..5c2158ae 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -42,8 +42,8 @@ let print_id_ofs p (id, ofs) =
 
 let print_eventval p = function
   | EVint n -> fprintf p "%ld" (camlint_of_coqint n)
-  | EVfloat f -> fprintf p "%F" (camlfloat_of_coqfloat f)
-  | EVsingle f -> fprintf p "%F" (camlfloat_of_coqfloat32 f)
+  | EVfloat f -> fprintf p "%.15F" (camlfloat_of_coqfloat f)
+  | EVsingle f -> fprintf p "%.15F" (camlfloat_of_coqfloat32 f)
   | EVlong n -> fprintf p "%LdLL" (camlint64_of_coqint n)
   | EVptr_global(id, ofs) -> fprintf p "&%a" print_id_ofs (id, ofs)
 
@@ -83,16 +83,16 @@ let name_of_fundef prog fd =
       if fd == fd' then extern_atom id else find_name rem
   | (id, Gvar v) :: rem ->
       find_name rem
-  in find_name prog.Csyntax.prog_defs
+  in find_name prog.Ctypes.prog_defs
 
 let name_of_function prog fn =
   let rec find_name = function
   | [] -> "<unknown function>"
-  | (id, Gfun(Csyntax.Internal fn')) :: rem ->
+  | (id, Gfun(Ctypes.Internal fn')) :: rem ->
       if fn == fn' then extern_atom id else find_name rem
   | (id, _) :: rem ->
       find_name rem
-  in find_name prog.Csyntax.prog_defs
+  in find_name prog.Ctypes.prog_defs
 
 let invert_local_variable e b =
   Maps.PTree.fold
@@ -581,7 +581,7 @@ let world_program prog =
         (id, Gvar gv')
     | Gfun fd ->
         (id, gd) in
- {prog with Csyntax.prog_defs = List.map change_def prog.Csyntax.prog_defs}
+ {prog with Ctypes.prog_defs = List.map change_def prog.Ctypes.prog_defs}
 
 (* Massaging the program to get a suitable "main" function *)
 
@@ -596,7 +596,7 @@ let change_main_function p old_main old_main_ty =
       fn_params = []; fn_vars = []; fn_body = body } in
   let new_main_id = intern_string "___main" in
   { prog_main = new_main_id;
-    Csyntax.prog_defs = (new_main_id, Gfun(Internal new_main_fn)) :: p.Csyntax.prog_defs;
+    Ctypes.prog_defs = (new_main_id, Gfun(Internal new_main_fn)) :: p.Ctypes.prog_defs;
     prog_public = p.prog_public;
     prog_types = p.prog_types;
     prog_comp_env = p.prog_comp_env }
@@ -607,7 +607,7 @@ let rec find_main_function name = function
   | (id, Gvar v) :: gdl -> find_main_function name gdl
 
 let fixup_main p =
-  match find_main_function p.Csyntax.prog_main p.prog_defs with
+  match find_main_function p.Ctypes.prog_main p.prog_defs with
   | None ->
       fprintf err_formatter "ERROR: no main() function@.";
       None