driver/Interp: update

Cherry-pick commit d1311e6 from trunk.
Simplify convert_external_arg so that it works both in 32 and 64 bits.

1 files changed, 8 insertions, 8 deletions

diff --git a/driver/Interp.ml b/driver/Interp.ml
index c197d004..1e328a70 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -304,7 +304,7 @@ let format_value m flags length conv arg =
       format_int64 (flags ^ conv) (camlint64_of_coqint i)
   | ('d'|'i'|'u'|'o'|'x'|'X'), ("ll"|"j"), _ ->
       "<long long argument expected"
-  | ('f'|'e'|'E'|'g'|'G'|'a'), "l", Vfloat f ->
+  | ('f'|'e'|'E'|'g'|'G'|'a'), (""|"l"), Vfloat f ->
       format_float (flags ^ conv) (camlfloat_of_coqfloat f)
   | ('f'|'e'|'E'|'g'|'G'|'a'), "", _ ->
       "<float argument expected"
@@ -366,14 +366,14 @@ let (>>=) opt f = match opt with None -> None | Some arg -> f arg
 (* Like eventval_of_val, but accepts static globals as well *)
 
 let convert_external_arg ge v t =
-  match v, t with
-  | Vint i, AST.Tint -> Some (EVint i)
-  | Vfloat f, AST.Tfloat -> Some (EVfloat f)
-  | Vsingle f, AST.Tsingle -> Some (EVsingle f)
-  | Vlong n, AST.Tlong -> Some (EVlong n)
-  | Vptr(b, ofs), AST.Tint ->
+  match v with
+  | Vint i -> Some (EVint i)
+  | Vfloat f -> Some (EVfloat f)
+  | Vsingle f -> Some (EVsingle f)
+  | Vlong n -> Some (EVlong n)
+  | Vptr(b, ofs) ->
       Senv.invert_symbol ge b >>= fun id -> Some (EVptr_global(id, ofs))
-  | _, _ -> None
+  | _ -> None
 
 let rec convert_external_args ge vl tl =
   match vl, tl with