aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/cbytegen.ml4
-rw-r--r--kernel/cemitcodes.ml7
-rw-r--r--kernel/nativecode.ml6
-rw-r--r--kernel/nativelambda.ml21
-rw-r--r--kernel/vm.ml6
-rw-r--r--lib/cList.ml2
-rw-r--r--plugins/funind/glob_termops.ml2
-rw-r--r--plugins/funind/indfun_common.ml5
-rw-r--r--plugins/funind/indfun_common.mli2
-rw-r--r--plugins/micromega/mutils.ml2
-rw-r--r--pretyping/cases.ml2
-rw-r--r--pretyping/program.ml2
-rw-r--r--proofs/tactic_debug.ml6
-rw-r--r--tactics/rewrite.ml48
-rw-r--r--tools/coqdoc/index.ml2
-rw-r--r--toplevel/classes.ml2
-rw-r--r--toplevel/indschemes.ml2
-rw-r--r--toplevel/obligations.ml6
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 =
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 19:46:45 +0000