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 | |
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
-rw-r--r-- | kernel/cbytegen.ml | 4 | ||||
-rw-r--r-- | kernel/cemitcodes.ml | 7 | ||||
-rw-r--r-- | kernel/nativecode.ml | 6 | ||||
-rw-r--r-- | kernel/nativelambda.ml | 21 | ||||
-rw-r--r-- | kernel/vm.ml | 6 | ||||
-rw-r--r-- | lib/cList.ml | 2 | ||||
-rw-r--r-- | plugins/funind/glob_termops.ml | 2 | ||||
-rw-r--r-- | plugins/funind/indfun_common.ml | 5 | ||||
-rw-r--r-- | plugins/funind/indfun_common.mli | 2 | ||||
-rw-r--r-- | plugins/micromega/mutils.ml | 2 | ||||
-rw-r--r-- | pretyping/cases.ml | 2 | ||||
-rw-r--r-- | pretyping/program.ml | 2 | ||||
-rw-r--r-- | proofs/tactic_debug.ml | 6 | ||||
-rw-r--r-- | tactics/rewrite.ml4 | 8 | ||||
-rw-r--r-- | tools/coqdoc/index.ml | 2 | ||||
-rw-r--r-- | toplevel/classes.ml | 2 | ||||
-rw-r--r-- | toplevel/indschemes.ml | 2 | ||||
-rw-r--r-- | toplevel/obligations.ml | 6 |
18 files changed, 39 insertions, 48 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 0f3636632..af6992252 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -497,8 +497,8 @@ let rec get_allias env kn = let rec compile_constr reloc c sz cont = match kind_of_term c with - | Meta _ -> raise (Invalid_argument "Cbytegen.compile_constr : Meta") - | Evar _ -> raise (Invalid_argument "Cbytegen.compile_constr : Evar") + | Meta _ -> invalid_arg "Cbytegen.compile_constr : Meta" + | Evar _ -> invalid_arg "Cbytegen.compile_constr : Evar" | Cast(c,_,_) -> compile_constr reloc c sz cont diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 90b4f0ae0..532f57866 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 diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 5bdb339d2..aeb5412e4 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 diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index b8580f2b3..154345ca2 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -437,7 +437,7 @@ module Vect = let extend v = if Int.equal v.size (Array.length v.elems) then let new_size = min (2*v.size) Sys.max_array_length in - if new_size <= v.size then raise (Invalid_argument "Vect.extend"); + if new_size <= v.size then invalid_arg "Vect.extend"; let new_elems = Array.make new_size v.elems.(0) in Array.blit v.elems 0 new_elems 0 (v.size); v.elems <- new_elems @@ -458,19 +458,16 @@ module Vect = let pop v = popn v 1 let get v n = - if v.size <= n then raise - (Invalid_argument "Vect.get:index out of bounds"); + if v.size <= n then invalid_arg "Vect.get:index out of bounds"; v.elems.(n) let get_last v n = - if v.size <= n then raise - (Invalid_argument "Vect.get:index out of bounds"); + if v.size <= n then invalid_arg "Vect.get:index out of bounds"; v.elems.(v.size - n - 1) let last v = - if Int.equal v.size 0 then raise - (Invalid_argument "Vect.last:index out of bounds"); + if Int.equal v.size 0 then invalid_arg "Vect.last:index out of bounds"; v.elems.(v.size - 1) let clear v = v.size <- 0 @@ -532,13 +529,13 @@ let empty_ids = [||] let rec lambda_of_constr env c = (* try *) match kind_of_term c with - | Meta _ -> raise (Invalid_argument "Nativelambda.lambda_of_constr: Meta") - | Evar _ -> raise (Invalid_argument "Nativelambda.lambda_of_constr : Evar") - + | Meta _ -> invalid_arg "Nativelambda.lambda_of_constr: Meta" + | Evar _ -> invalid_arg "Nativelambda.lambda_of_constr : Evar" + | Cast (c, _, _) -> lambda_of_constr env c - + | Rel i -> Renv.get env i - + | Var id -> Lvar id | Sort s -> Lsort s 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 *) diff --git a/lib/cList.ml b/lib/cList.ml index 78c17c3ff..8e031a0c9 100644 --- a/lib/cList.ml +++ b/lib/cList.ml @@ -788,7 +788,7 @@ let rec combine3 x y z = | [], [], [] -> [] | (x :: xs), (y :: ys), (z :: zs) -> (x, y, z) :: combine3 xs ys zs - | _, _, _ -> raise (Invalid_argument "List.combine3") + | _, _, _ -> invalid_arg "List.combine3" (* Keep only those products that do not return None *) diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 868bf58c9..0159a0aee 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -108,7 +108,7 @@ let glob_make_or t1 t2 = mkGApp (mkGRef(Lazy.force Coqlib.coq_or_ref),[t1;t2]) to [P1 \/ ( .... \/ Pn)] *) let rec glob_make_or_list = function - | [] -> raise (Invalid_argument "mk_or") + | [] -> invalid_arg "mk_or" | [e] -> e | e::l -> glob_make_or e (glob_make_or_list l) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 8305c4735..67f6fdd54 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -13,9 +13,6 @@ let mk_equation_id id = Nameops.add_suffix id "_equation" let msgnl m = () -let invalid_argument s = raise (Invalid_argument s) - - let fresh_id avoid s = Namegen.next_ident_away_in_goal (Id.of_string s) avoid let fresh_name avoid s = Name (fresh_id avoid s) @@ -30,7 +27,7 @@ let array_get_start a = (Array.length a - 1) (fun i -> a.(i)) with Invalid_argument "index out of bounds" -> - invalid_argument "array_get_start" + invalid_arg "array_get_start" let id_of_name = function Name id -> id diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index d9f0f51ce..6f47e2289 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -13,8 +13,6 @@ val mk_equation_id : Id.t -> Id.t val msgnl : std_ppcmds -> unit -val invalid_argument : string -> 'a - val fresh_id : Id.t list -> string -> Id.t val fresh_name : Id.t list -> string -> Name.t val get_name : Id.t list -> ?default:string -> Name.t -> Name.t diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index 240c29e0f..43cad05e9 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -72,7 +72,7 @@ let rec map3 f l1 l2 l3 = match l1 , l2 ,l3 with | [] , [] , [] -> [] | e1::l1 , e2::l2 , e3::l3 -> (f e1 e2 e3)::(map3 f l1 l2 l3) - | _ -> raise (Invalid_argument "map3") + | _ -> invalid_arg "map3" let rec is_sublist l1 l2 = match l1 ,l2 with diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 358cc2f03..7516951e8 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1958,7 +1958,7 @@ let vars_of_ctx ctx = [hole; GVar (Loc.ghost, prev)])) :: vars | _ -> match na with - Anonymous -> raise (Invalid_argument "vars_of_ctx") + Anonymous -> invalid_arg "vars_of_ctx" | Name n -> n, GVar (Loc.ghost, n) :: vars) ctx (Id.of_string "vars_of_ctx_error", []) in List.rev y diff --git a/pretyping/program.ml b/pretyping/program.ml index a701fdef4..6d913060b 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -55,7 +55,7 @@ let mk_coq_not x = mkApp (delayed_force coq_not, [| x |]) let unsafe_fold_right f = function hd :: tl -> List.fold_right f tl hd - | [] -> raise (Invalid_argument "unsafe_fold_right") + | [] -> invalid_arg "unsafe_fold_right" let mk_coq_and l = let and_typ = delayed_force coq_and in diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index afbc8bbe4..5952fd29c 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -91,14 +91,14 @@ let run_com inst = let s = String.sub inst i (String.length inst - i) in if inst.[0] >= '0' && inst.[0] <= '9' then let num = int_of_string s in - if num<0 then raise (Invalid_argument "run_com"); + if num<0 then invalid_arg "run_com"; skip:=num;skipped:=0 else breakpoint:=Some (possibly_unquote s) else - raise (Invalid_argument "run_com") + invalid_arg "run_com" else - raise (Invalid_argument "run_com") + invalid_arg "run_com" (* Prints the run counter *) let run ini = diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index f7f52de70..20bcb84a7 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -471,8 +471,8 @@ let rec decomp_pointwise n c = decomp_pointwise (pred n) relb | App (f, [| a; b; arelb |]) when eq_constr f (Lazy.force forall_relation) -> decomp_pointwise (pred n) (Reductionops.beta_applist (arelb, [mkRel 1])) - | _ -> raise (Invalid_argument "decomp_pointwise") - + | _ -> invalid_arg "decomp_pointwise" + let rec apply_pointwise rel = function | arg :: args -> (match kind_of_term rel with @@ -480,7 +480,7 @@ let rec apply_pointwise rel = function apply_pointwise relb args | App (f, [| a; b; arelb |]) when eq_constr f (Lazy.force forall_relation) -> apply_pointwise (Reductionops.beta_applist (arelb, [arg])) args - | _ -> raise (Invalid_argument "apply_pointwise")) + | _ -> invalid_arg "apply_pointwise") | [] -> rel let pointwise_or_dep_relation n t car rel = @@ -577,7 +577,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' cstr evars let evars, morph_instance, proj, sigargs, m', args, args' = let first = match (Array.findi (fun _ b -> not (Option.is_empty b)) args') with | Some i -> i - | None -> raise (Invalid_argument "resolve_morphism") in + | None -> invalid_arg "resolve_morphism" in let morphargs, morphobjs = Array.chop first args in let morphargs', morphobjs' = Array.chop first args' in let appm = mkApp(m, morphargs) in diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index ba71785c8..7368ac1e0 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -288,7 +288,7 @@ let type_of_string = function | "mod" | "modtype" -> Module | "tac" -> TacticDefinition | "sec" -> Section - | s -> raise (Invalid_argument ("type_of_string:" ^ s)) + | s -> invalid_arg ("type_of_string:" ^ s) let ill_formed_glob_file f = eprintf "Warning: ill-formed file %s (links will not be available)\n" f diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 570e66deb..8bb7c859f 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -308,7 +308,7 @@ let named_of_rel_context l = let acc, ctx = List.fold_right (fun (na, b, t) (subst, ctx) -> - let id = match na with Anonymous -> raise (Invalid_argument "named_of_rel_context") | Name id -> id in + let id = match na with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in let d = (id, Option.map (substl subst) b, substl subst t) in (mkVar id :: subst, d :: ctx)) l ([], []) diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index a0300738b..3aaf49548 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -400,7 +400,7 @@ let list_split_rev_at index l = in aux 0 [] l let fold_left' f = function - [] -> raise (Invalid_argument "fold_left'") + [] -> invalid_arg "fold_left'" | hd :: tl -> List.fold_left f hd tl let build_combined_scheme env schemes = diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 765ffae95..b52a7b2cd 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -167,9 +167,9 @@ let evar_dependencies evm oev = Int.Set.fold (fun ev s -> let evi = Evd.find evm ev in let deps' = evars_of_evar_info evi in - if Int.Set.mem oev deps' then - raise (Invalid_argument ("Ill-formed evar map: cycle detected for evar " ^ string_of_int oev)) - else Int.Set.union deps' s) + if Int.Set.mem oev deps' then + invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ string_of_int oev) + else Int.Set.union deps' s) deps deps in let rec aux deps = |