diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-12 23:59:05 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-12 23:59:05 +0000 |
| commit | 3b7ecfa6d4da684a635b2469c2d9a2e1e0ed0807 (patch) | |
| tree | 2ce23cad6a0067480658001f0636efbdd3269b51 /kernel/vm.ml | |
| parent | b66d099bdda2ce1cfaeeb7938346a348ef4d40cd (diff) | |
invalid_arg instead of raise (Invalid_argement ...)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16270 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/vm.ml')
| -rw-r--r-- | kernel/vm.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/vm.ml b/kernel/vm.ml index c6491c479..bc7116a35 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -249,9 +249,9 @@ let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2 let arg args i = if 0 <= i && i < (nargs args) then val_of_obj (Obj.field (Obj.repr args) (i+2)) - else raise (Invalid_argument + else invalid_arg ("Vm.arg size = "^(string_of_int (nargs args))^ - " acces "^(string_of_int i))) + " acces "^(string_of_int i)) let apply_arguments vf vargs = let n = nargs vargs in @@ -488,7 +488,7 @@ let btag : vblock -> int = fun b -> Obj.tag (Obj.repr b) let bsize : vblock -> int = fun b -> Obj.size (Obj.repr b) let bfield b i = if 0 <= i && i < (bsize b) then val_of_obj (Obj.field (Obj.repr b) i) - else raise (Invalid_argument "Vm.bfield") + else invalid_arg "Vm.bfield" (* Functions over vswitch *) |