Restrict (try...with...) to avoid catching critical exn (part 5)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16281 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 15 insertions, 10 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 3a27116222..20cf9edb87 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -123,7 +123,7 @@ let non_trivial = function
 
 let patterns_of_constr env sigma nrels term=
   let f,args=
-    try destApp (whd_delta env term) with _ -> raise Not_found in
+    try destApp (whd_delta env term) with DestKO -> raise Not_found in
 	if eq_constr f (Lazy.force _eq) && (Array.length args)=3
 	then
 	  let patt1,rels1 = pattern_of_constr env sigma args.(1)
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index 1187d9d760..8c5aec38bf 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -74,7 +74,7 @@ let mode_of_pftreestate pts =
 let get_current_mode () =
   try 
     mode_of_pftreestate (Pfedit.get_pftreestate ())
-  with _ -> Mode_none
+  with Proof_global.NoCurrentProof -> Mode_none
 
 let check_not_proof_mode str =
  if get_current_mode () = Mode_proof then
diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli
index 538d8944d7..c54dcdc281 100644
--- a/plugins/decl_mode/decl_mode.mli
+++ b/plugins/decl_mode/decl_mode.mli
@@ -70,6 +70,8 @@ val get_stack : Proof.proof -> stack_info list
 val get_top_stack : Proof.proof -> stack_info list
 
 val get_last:  Environ.env -> Id.t
+(** [get_last] raises a [UserError] when it cannot find a previous
+    statement in the environment. *)
 
 val focus : Proof.proof -> unit
 
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index dc51c23849..1ae8419c83 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -366,7 +366,7 @@ let find_subsubgoal c ctyp skip submetas gls =
 		  se.se_meta submetas se.se_meta_list}
 	  else
 	      dfs (pred n)
-      with _ ->
+      with e when Errors.noncritical e ->
 	begin
 	  enstack_subsubgoals env se stack gls;
 	  dfs n
@@ -451,11 +451,12 @@ let mk_stat_or_thesis info gls = function
   | Thesis Plain -> pf_concl gls
 
 let just_tac _then cut info gls0 = 
-  let last_item = if _then then 
-      let last_id = try get_last (pf_env gls0) with Failure _ -> 
-		error "\"then\" and \"hence\" require at least one previous fact"  in
-		[mkVar last_id]
-	    else []  
+  let last_item =
+    if _then then
+      try [mkVar (get_last (pf_env gls0))]
+      with UserError _ ->
+	error "\"then\" and \"hence\" require at least one previous fact"
+    else []
   in
   let items_tac gls = 
     match cut.cut_by with
@@ -504,7 +505,9 @@ let decompose_eq id gls =
 
 let instr_rew _thus rew_side cut gls0 =
   let last_id =
-    try get_last (pf_env gls0) with _ -> error "No previous equality." in
+    try get_last (pf_env gls0)
+    with UserError _ -> error "No previous equality."
+  in
   let typ,lhs,rhs = decompose_eq last_id gls0 in
   let items_tac gls =
     match cut.cut_by with
@@ -834,7 +837,7 @@ let build_per_info etype casee gls =
   let ind =
     try
       destInd hd
-    with _ ->
+    with DestKO ->
       error "Case analysis must be done on an inductive object." in
   let mind,oind = Global.lookup_inductive ind in
   let nparams,index =