1 files changed, 43 insertions, 18 deletions

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 1a8ec6d6f..32a3b53fd 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -128,7 +128,7 @@ let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) =
   let wit = Genarg.create_arg "tacvalue" in
   let () = register_val0 wit None in
   let () = Genprint.register_val_print0 (base_val_typ wit)
-             (fun _ -> Genprint.PrinterBasic (fun () -> str "<tactic closure>")) in
+             (fun _ -> Genprint.TopPrinterBasic (fun () -> str "<tactic closure>")) in
   wit
 
 let of_tacvalue v = in_gen (topwit wit_tacvalue) v
@@ -242,9 +242,9 @@ let pr_value env v =
     | None -> str "a value of type" ++ spc () ++ pr_argument_type v in
   let open Genprint in
   match generic_val_print v with
-  | PrinterBasic pr -> pr ()
-  | PrinterNeedsContext pr -> pr_with_env pr
-  | PrinterNeedsContextAndLevel { default_already_surrounded; printer } ->
+  | TopPrinterBasic pr -> pr ()
+  | TopPrinterNeedsContext pr -> pr_with_env pr
+  | TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } ->
      pr_with_env (fun env sigma -> printer env sigma default_already_surrounded)
 
 let pr_closure env ist body =
@@ -420,7 +420,7 @@ let interp_hyp ist env sigma (loc,id as locid) =
   with Not_found ->
   (* Then look if bound in the proof context at calling time *)
   if is_variable env id then id
-  else Loc.raise ?loc (Logic.RefinerError (Logic.NoSuchHyp id))
+  else Loc.raise ?loc (Logic.RefinerError (env, sigma, Logic.NoSuchHyp id))
 
 let interp_hyp_list_as_list ist env sigma (loc,id as x) =
   try coerce_to_hyp_list env sigma (Id.Map.find id ist.lfun)
@@ -821,9 +821,9 @@ let message_of_value v =
     Ftactic.enter begin fun gl -> Ftactic.return (pr (pf_env gl) (project gl)) end in
   let open Genprint in
   match generic_val_print v with
-  | PrinterBasic pr -> Ftactic.return (pr ())
-  | PrinterNeedsContext pr -> pr_with_env pr
-  | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+  | TopPrinterBasic pr -> Ftactic.return (pr ())
+  | TopPrinterNeedsContext pr -> pr_with_env pr
+  | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
      pr_with_env (fun env sigma -> printer env sigma default_ensure_surrounded)
 
 let interp_message_token ist = function
@@ -1040,7 +1040,7 @@ let eval_pattern lfun ist env sigma (bvars,(glob,_),pat as c) =
     (bvars,instantiate_pattern env sigma lfun pat)
 
 let read_pattern lfun ist env sigma = function
-  | Subterm (b,ido,c) -> Subterm (b,ido,eval_pattern lfun ist env sigma c)
+  | Subterm (ido,c) -> Subterm (ido,eval_pattern lfun ist env sigma c)
   | Term c -> Term (eval_pattern lfun ist env sigma c)
 
 (* Reads the hypotheses of a Match Context rule *)
@@ -1353,8 +1353,8 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
         begin
           let open Genprint in
           match generic_val_print v with
-          | PrinterBasic _ -> call_debug None
-          | PrinterNeedsContext _ | PrinterNeedsContextAndLevel _ ->
+          | TopPrinterBasic _ -> call_debug None
+          | TopPrinterNeedsContext _ | TopPrinterNeedsContextAndLevel _ ->
              Proofview.Goal.enter (fun gl -> call_debug (Some (pf_env gl,project gl)))
         end <*>
         if List.is_empty lval then Ftactic.return v else interp_app loc ist v lval
@@ -1380,13 +1380,38 @@ and tactic_of_value ist vle =
         extra = TacStore.set ist.extra f_trace []; } in
       let tac = name_if_glob appl (eval_tactic ist t) in
       Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac trace tac)
-  | VFun (_, _, _,vars,_) ->
-    let numargs = List.length vars in
-    Tacticals.New.tclZEROMSG
-      (str "A fully applied tactic is expected:" ++ spc() ++ Pp.str "missing " ++
-       Pp.str (String.plural numargs "argument") ++ Pp.str " for " ++
-       Pp.str (String.plural numargs "variable") ++ Pp.str " " ++
-       pr_enum Name.print vars ++ Pp.str ".")
+  | VFun (appl,_,vmap,vars,_) ->
+     let tactic_nm =
+       match appl with
+         UnnamedAppl -> "An unnamed user-defined tactic"
+       | GlbAppl apps ->
+          let nms = List.map (fun (kn,_) -> Names.KerName.to_string kn) apps in
+          match nms with
+            []    -> assert false
+          | kn::_ -> "The user-defined tactic \"" ^ kn ^ "\"" (* TODO: when do we not have a singleton? *)
+     in
+     let numargs = List.length vars in
+     let givenargs =
+       List.map (fun (arg,_) -> Names.Id.to_string arg) (Names.Id.Map.bindings vmap) in
+     let numgiven = List.length givenargs in
+     Tacticals.New.tclZEROMSG
+       (Pp.str tactic_nm ++ Pp.str " was not fully applied:" ++ spc() ++
+          (match numargs with
+            0 -> assert false
+          | 1 ->
+             Pp.str "There is a missing argument for variable " ++
+               (Name.print (List.hd vars))
+          | _ -> Pp.str "There are missing arguments for variables " ++
+             pr_enum Name.print vars) ++ Pp.pr_comma () ++
+          match numgiven with
+            0 ->
+              Pp.str "no arguments at all were provided."
+          | 1 ->
+             Pp.str "an argument was provided for variable " ++
+               Pp.str (List.hd givenargs) ++ Pp.str "."
+          | _ ->
+             Pp.str "arguments were provided for variables " ++
+               pr_enum Pp.str givenargs ++ Pp.str ".")
   | VRec _ -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.")
   else if has_type vle (topwit wit_tactic) then
     let tac = out_gen (topwit wit_tactic) vle in