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.

4 files changed, 10 insertions, 9 deletions

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)