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/nativecode.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/nativecode.ml')
| -rw-r--r-- | kernel/nativecode.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 5bdb339d2a..aeb5412e44 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -399,7 +399,7 @@ let get_prod_name codom = let get_lname (_,l) = match l with | MLlocal id -> id - | _ -> raise (Invalid_argument "Nativecode.get_lname") + | _ -> invalid_arg "Nativecode.get_lname" let fv_params env = let fvn, fvr = !(env.env_named), !(env.env_urel) in @@ -1401,8 +1401,8 @@ let compile_mind_deps env prefix ~interactive reverse order, as well as linking information updates *) let rec compile_deps env prefix ~interactive init t = match kind_of_term t with - | Meta _ -> raise (Invalid_argument "Nativecode.get_deps: Meta") - | Evar _ -> raise (Invalid_argument "Nativecode.get_deps: Evar") + | Meta _ -> invalid_arg "Nativecode.get_deps: Meta" + | Evar _ -> invalid_arg "Nativecode.get_deps: Evar" | Ind (mind,_) -> compile_mind_deps env prefix ~interactive init mind | Const c -> let c = get_allias env c in |