diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/cc/cctac.ml | 4 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_mode.ml | 7 | ||||
| -rw-r--r-- | plugins/firstorder/ground.ml | 3 | ||||
| -rw-r--r-- | plugins/rtauto/refl_tauto.ml | 2 |
4 files changed, 7 insertions, 9 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 9a2f23d64..3a2711622 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -220,9 +220,7 @@ let make_prb gls depth additionnal_terms = let build_projection intype outtype (cstr:constructor) special default gls= let env=pf_env gls in - let (h,argv) = - try destApp intype with - Invalid_argument _ -> (intype,[||]) in + let (h,argv) = try destApp intype with DestKO -> (intype,[||]) in let ind=destInd h in let types=Inductiveops.arities_of_constructors env ind in let lp=Array.length types in diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index 8b5fe85e7..1187d9d76 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -113,8 +113,7 @@ let get_top_stack pts = let info = get_info sigma gl in info.pm_stack -let get_last env = - try - let (id,_,_) = List.hd (Environ.named_context env) in id - with Invalid_argument _ -> error "no previous statement to use" +let get_last env = match Environ.named_context env with + | (id,_,_)::_ -> id + | [] -> error "no previous statement to use" diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index 48e60d798..6c1709140 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -20,7 +20,8 @@ let update_flags ()= try let kn=destConst (Classops.get_coercion_value coe) in predref:=Names.Cpred.add kn !predref - with Invalid_argument "destConst"-> () in + with DestKO -> () + in List.iter f (Classops.coercions ()); red_flags:= Closure.RedFlags.red_add_transparent diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index ceaf2a79b..597b6afb6 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -122,7 +122,7 @@ let rec make_form atom_env gls term = let fb=make_form atom_env gls argv.(1) in Disjunct (fa,fb) else make_atom atom_env (normalize term) - with Invalid_argument _ -> make_atom atom_env (normalize term) + with DestKO -> make_atom atom_env (normalize term) end | _ -> make_atom atom_env (normalize term) |