diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-12 23:59:08 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-12 23:59:08 +0000 |
| commit | 6d5eee245a85f410ec184353ab9f38ce3aa4e331 (patch) | |
| tree | 9260a0fb3662dbeb6837468e30f69f5f862e7893 /plugins | |
| parent | 3b7ecfa6d4da684a635b2469c2d9a2e1e0ed0807 (diff) | |
Term.dest* functions now raise specific DestKO exn instead of Invalid_argument
**Warning** the ml code of plugins may have to be adapted after this.
Concerning coq itself, I've done the adaptations, let's hope I've
forgotten none. In practice, the number of changes are relatively low,
and the code is quite cleaner this way.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16271 85f007b7-540e-0410-9357-904b9bb8a0f7
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) |