diff options
| author | letouzey | 2013-03-12 23:59:05 +0000 |
|---|---|---|
| committer | letouzey | 2013-03-12 23:59:05 +0000 |
| commit | 3b7ecfa6d4da684a635b2469c2d9a2e1e0ed0807 (patch) | |
| tree | 2ce23cad6a0067480658001f0636efbdd3269b51 /kernel/cemitcodes.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/cemitcodes.ml')
| -rw-r--r-- | kernel/cemitcodes.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 90b4f0ae07..532f57866c 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -61,8 +61,7 @@ let out_word b1 b2 b3 b4 = then 2 * len else if len = Sys.max_string_length - then raise (Invalid_argument "String.create") (* Pas la bonne execption -.... *) + then invalid_arg "String.create" (* Pas la bonne exception .... *) else Sys.max_string_length in let new_buffer = String.create new_len in String.blit !out_buffer 0 new_buffer 0 len; @@ -214,7 +213,7 @@ let emit_instr = function | Kconst c -> out opGETGLOBAL; slot_for_const c | Kmakeblock(n, t) -> - if Int.equal n 0 then raise (Invalid_argument "emit_instr : block size = 0") + if Int.equal n 0 then invalid_arg "emit_instr : block size = 0" else if n < 4 then (out(opMAKEBLOCK1 + n - 1); out_int t) else (out opMAKEBLOCK; out_int n; out_int t) | Kmakeprod -> @@ -237,7 +236,7 @@ let emit_instr = function | Ksetfield n -> if n <= 1 then out (opSETFIELD0+n) else (out opSETFIELD;out_int n) - | Ksequence _ -> raise (Invalid_argument "Cemitcodes.emit_instr") + | Ksequence _ -> invalid_arg "Cemitcodes.emit_instr" (* spiwack *) | Kbranch lbl -> out opBRANCH; out_label lbl | Kaddint31 -> out opADDINT31 |