Attempt to improve error message when "apply in" fail.

- Adding a better location in the "apply" on the fly pattern.
- Printing statement of lemma and of hypothesis.

Was suggested by discussion at wish report #5390.

7 files changed, 33 insertions, 19 deletions

diff --git a/intf/misctypes.mli b/intf/misctypes.mli
index e4f595ac4a..33dc2a335c 100644
--- a/intf/misctypes.mli
+++ b/intf/misctypes.mli
@@ -28,7 +28,7 @@ and 'constr intro_pattern_action_expr =
   | IntroWildcard
   | IntroOrAndPattern of 'constr or_and_intro_pattern_expr
   | IntroInjection of (Loc.t * 'constr intro_pattern_expr) list
-  | IntroApplyOn of 'constr * (Loc.t * 'constr intro_pattern_expr)
+  | IntroApplyOn of (Loc.t * 'constr) * (Loc.t * 'constr intro_pattern_expr)
   | IntroRewrite of bool
 and 'constr or_and_intro_pattern_expr =
   | IntroOrPattern of (Loc.t * 'constr intro_pattern_expr) list list
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 685c07c9a8..fa01baab75 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -325,8 +325,9 @@ GEXTEND Gram
         l = LIST0 ["%"; c = operconstr LEVEL "0" -> c] ->
           let loc0,pat = pat in
           let f c pat =
-            let loc = Loc.merge loc0 (Constrexpr_ops.constr_loc c) in
-            IntroAction (IntroApplyOn (c,(loc,pat))) in
+            let loc1 = Constrexpr_ops.constr_loc c in
+            let loc = Loc.merge loc0 loc1 in
+            IntroAction (IntroApplyOn ((loc1,c),(loc,pat))) in
           !@loc, List.fold_right f l pat ] ]
   ;
   simple_intropattern_closed:
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 1a8f26b264..3f83f104e9 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -248,8 +248,8 @@ and intern_intro_pattern_action lf ist = function
   | IntroInjection l ->
       IntroInjection (List.map (intern_intro_pattern lf ist) l)
   | IntroWildcard | IntroRewrite _ as x -> x
-  | IntroApplyOn (c,pat) ->
-      IntroApplyOn (intern_constr ist c, intern_intro_pattern lf ist pat)
+  | IntroApplyOn ((loc,c),pat) ->
+      IntroApplyOn ((loc,intern_constr ist c), intern_intro_pattern lf ist pat)
 
 and intern_or_and_intro_pattern lf ist = function
    | IntroAndPattern l ->
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index aa646aa517..61a70d712d 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -520,7 +520,7 @@ let rec intropattern_ids (loc,pat) = match pat with
       List.flatten (List.map intropattern_ids (List.flatten ll))
   | IntroAction (IntroInjection l) ->
       List.flatten (List.map intropattern_ids l)
-  | IntroAction (IntroApplyOn (c,pat)) -> intropattern_ids pat
+  | IntroAction (IntroApplyOn ((_,c),pat)) -> intropattern_ids pat
   | IntroNaming (IntroAnonymous | IntroFresh _)
   | IntroAction (IntroWildcard | IntroRewrite _)
   | IntroForthcoming _ -> []
@@ -913,14 +913,14 @@ and interp_intro_pattern_action ist env sigma = function
   | IntroInjection l ->
       let sigma,l = interp_intro_pattern_list_as_list ist env sigma l in
       sigma, IntroInjection l
-  | IntroApplyOn (c,ipat) ->
+  | IntroApplyOn ((loc,c),ipat) ->
       let c = { delayed = fun env sigma ->
         let sigma = Sigma.to_evar_map sigma in
         let (sigma, c) = interp_open_constr ist env sigma c in
         Sigma.Unsafe.of_pair (c, sigma)
       } in
       let sigma,ipat = interp_intro_pattern ist env sigma ipat in
-      sigma, IntroApplyOn (c,ipat)
+      sigma, IntroApplyOn ((loc,c),ipat)
   | IntroWildcard | IntroRewrite _ as x -> sigma, x
 
 and interp_or_and_intro_pattern ist env sigma = function
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index b09bdda65c..fe3a9f3b2a 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -51,8 +51,8 @@ let rec subst_intro_pattern subst = function
   | loc, IntroNaming _ | loc, IntroForthcoming _ as x -> x
 
 and subst_intro_pattern_action subst = function
-  | IntroApplyOn (t,pat) ->
-      IntroApplyOn (subst_glob_constr subst t,subst_intro_pattern subst pat)
+  | IntroApplyOn ((loc,t),pat) ->
+      IntroApplyOn ((loc,subst_glob_constr subst t),subst_intro_pattern subst pat)
   | IntroOrAndPattern l ->
       IntroOrAndPattern (subst_intro_or_and_pattern subst l)
   | IntroInjection l -> IntroInjection (List.map (subst_intro_pattern subst) l)
diff --git a/printing/miscprint.ml b/printing/miscprint.ml
index 7b2c5695fd..360843711c 100644
--- a/printing/miscprint.ml
+++ b/printing/miscprint.ml
@@ -28,7 +28,7 @@ and pr_intro_pattern_action prc = function
   | IntroInjection pl ->
       str "[=" ++ hv 0 (prlist_with_sep spc (pr_intro_pattern prc) pl) ++
       str "]"
-  | IntroApplyOn (c,pat) -> pr_intro_pattern prc pat ++ str "%" ++ prc c
+  | IntroApplyOn ((_,c),pat) -> pr_intro_pattern prc pat ++ str "%" ++ prc c
   | IntroRewrite true -> str "->"
   | IntroRewrite false -> str "<-"
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6205bd1092..84d09d8330 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1815,24 +1815,37 @@ let find_matching_clause unifier clause =
     with NotExtensibleClause -> failwith "Cannot apply"
   in find clause
 
+exception UnableToApply
+
 let progress_with_clause flags innerclause clause =
   let ordered_metas = List.rev (clenv_independent clause) in
-  if List.is_empty ordered_metas then error "Statement without assumptions.";
+  if List.is_empty ordered_metas then raise UnableToApply;
   let f mv =
     try Some (find_matching_clause (clenv_fchain ~with_univs:false mv ~flags clause) innerclause)
     with Failure _ -> None
   in
   try List.find_map f ordered_metas
-  with Not_found -> error "Unable to unify."
+  with Not_found -> raise UnableToApply
+
+let explain_unable_to_apply_lemma loc env sigma thm innerclause =
+  user_err ~loc (hov 0
+    (Pp.str "Unable to apply lemma of type" ++ brk(1,1) ++
+     Pp.quote (Printer.pr_lconstr_env env sigma thm) ++ spc() ++
+     str "on hypothesis of type" ++ brk(1,1) ++
+     Pp.quote (Printer.pr_lconstr_env innerclause.env innerclause.evd (clenv_type innerclause)) ++
+     str "."))
 
-let apply_in_once_main flags innerclause env sigma (d,lbind) =
+let apply_in_once_main flags innerclause env sigma (loc,d,lbind) =
   let thm = nf_betaiota sigma (Retyping.get_type_of env sigma d) in
   let rec aux clause =
     try progress_with_clause flags innerclause clause
     with e when CErrors.noncritical e ->
-    let e = CErrors.push e in
+    let e' = CErrors.push e in
     try aux (clenv_push_prod clause)
-    with NotExtensibleClause -> iraise e
+    with NotExtensibleClause ->
+      match e with
+      | UnableToApply -> explain_unable_to_apply_lemma loc env sigma thm innerclause
+      | _ -> iraise e'
   in
   aux (make_clenv_binding env sigma (d,thm) lbind)
 
@@ -1852,7 +1865,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     try
-      let clause = apply_in_once_main flags innerclause env sigma (c,lbind) in
+      let clause = apply_in_once_main flags innerclause env sigma (loc,c,lbind) in
       clenv_refine_in ~sidecond_first with_evars targetid id sigma clause
         (fun id ->
           Tacticals.New.tclTHENLIST [
@@ -2467,7 +2480,7 @@ and intro_pattern_action loc with_evars b style pat thin destopt tac id =
       intro_decomp_eq loc l' thin tac id
   | IntroRewrite l2r ->
       rewrite_hyp_then style with_evars thin l2r id (fun thin -> tac thin None [])
-  | IntroApplyOn (f,(loc,pat)) ->
+  | IntroApplyOn ((loc',f),(loc,pat)) ->
       let naming,tac_ipat =
         prepare_intros_loc loc with_evars (IntroIdentifier id) destopt pat in
       let doclear =
@@ -2479,7 +2492,7 @@ and intro_pattern_action loc with_evars b style pat thin destopt tac id =
         let Sigma (c, sigma, p) = f.delayed env sigma in
         Sigma ((c, NoBindings), sigma, p)
       } in
-      apply_in_delayed_once false true true with_evars naming id (None,(loc,f))
+      apply_in_delayed_once false true true with_evars naming id (None,(loc',f))
         (fun id -> Tacticals.New.tclTHENLIST [doclear; tac_ipat id; tac thin None []])
 
 and prepare_intros_loc loc with_evars dft destopt = function