Normalizing exception raised by tactic coercions.

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

2 files changed, 18 insertions, 17 deletions

diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index f00f555278..d5b3986aff 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -79,7 +79,7 @@ let coerce_to_constr_context v =
   let v = Value.normalize v in
   if has_type v (topwit wit_constr_context) then
     out_gen (topwit wit_constr_context) v
-  else errorlabstrm "coerce_to_constr_context" (str "Not a context variable.")
+  else raise (CannotCoerceTo "a term context")
 
 (* Interprets an identifier which must be fresh *)
 let coerce_to_ident fresh env v =
@@ -124,20 +124,22 @@ let coerce_to_int v =
 
 let coerce_to_constr env v =
   let v = Value.normalize v in
+  let fail () = raise (CannotCoerceTo "a term") in
   if has_type v (topwit wit_intro_pattern) then
     match out_gen (topwit wit_intro_pattern) v with
-    | _, IntroIdentifier id -> ([],constr_of_id env id)
-    | _ -> raise Not_found
+    | _, IntroIdentifier id ->
+      (try ([], constr_of_id env id) with Not_found -> fail ())
+    | _ -> fail ()
   else if has_type v (topwit wit_constr) then
     let c = out_gen (topwit wit_constr) v in
     ([], c)
   else if has_type v (topwit wit_constr_under_binders) then
     out_gen (topwit wit_constr_under_binders) v
-  else raise Not_found
+  else fail ()
 
 let coerce_to_closed_constr env v =
   let ids,c = coerce_to_constr env v in
-  if not (List.is_empty ids) then raise Not_found;
+  let () = if not (List.is_empty ids) then raise (CannotCoerceTo "a term") in
   c
 
 let coerce_to_evaluable_ref env v =
@@ -161,11 +163,11 @@ let coerce_to_constr_list env v =
   | Some l ->
     let map v = coerce_to_closed_constr env v in
     List.map map l
-  | None -> raise Not_found
+  | None -> raise (CannotCoerceTo "a term list")
 
 let coerce_to_intro_pattern_list loc env v =
   match Value.to_list v with
-  | None -> raise Not_found
+  | None -> raise (CannotCoerceTo "an intro pattern list")
   | Some l ->
     let map v = (loc, coerce_to_intro_pattern env v) in
     List.map map l
@@ -187,7 +189,7 @@ let coerce_to_hyp_list env v =
   | Some l ->
     let map n = coerce_to_hyp env n in
     List.map map l
-  | None -> raise Not_found
+  | None -> raise (CannotCoerceTo "a variable list")
 
 (* Interprets a qualified name *)
 let coerce_to_reference env v =
@@ -233,7 +235,7 @@ let coerce_to_decl_or_quant_hyp env v =
 
 let coerce_to_int_or_var_list v =
   match Value.to_list v with
-  | None -> raise Not_found
+  | None -> raise (CannotCoerceTo "an int list")
   | Some l ->
     let map n = ArgArg (coerce_to_int n) in
     List.map map l
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 0df40d05be..5371611c5d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -404,7 +404,7 @@ let extract_ltac_constr_values ist env =
     try
       let c = coerce_to_constr env v in
       (Id.Map.add id c vars1, vars2)
-    with Not_found ->
+    with CannotCoerceTo _ ->
       let ido =
         let v = Value.normalize v in
         if has_type v (topwit wit_intro_pattern) then
@@ -543,8 +543,8 @@ let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l =
         List.map inj_fun (coerce_to_constr_list env (List.assoc id ist.lfun))
     | _ ->
         raise Not_found
-    with Not_found ->
-      (*all of dest_fun, List.assoc, coerce_to_constr_list may raise Not_found*)
+    with CannotCoerceTo _ | Not_found ->
+      (* dest_fun, List.assoc may raise Not_found *)
       let sigma, c = interp_fun ist env sigma x in
       sigma, [c] in
   let sigma, l = List.fold_map try_expand_ltac_var sigma l in
@@ -1531,14 +1531,13 @@ and interp_ltac_constr ist gl e =
     raise Not_found in
   let result = Value.normalize result in
   try
-    let cresult = coerce_to_constr (pf_env gl) result in
+    let cresult = coerce_to_closed_constr (pf_env gl) result in
     debugging_step ist (fun () ->
       Pptactic.pr_glob_tactic (pf_env gl) e ++ fnl() ++
       str " has value " ++ fnl() ++
-      pr_constr_under_binders_env (pf_env gl) cresult);
-    if not (List.is_empty (fst cresult)) then raise Not_found;
-    sigma , snd cresult
-  with Not_found ->
+      pr_constr_env (pf_env gl) cresult);
+    sigma, cresult
+  with CannotCoerceTo _ ->
     errorlabstrm ""
       (str "Must evaluate to a closed term" ++ fnl() ++
 	  str "offending expression: " ++ fnl() ++