diff options
Diffstat (limited to 'plugins')
| -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 |
4 files changed, 3 insertions, 8 deletions
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 868bf58c96..0159a0aeeb 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 8305c47350..67f6fdd543 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 d9f0f51cee..6f47e22893 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 240c29e0ff..43cad05e94 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 |
