Merge PR #6047: A generic printer for ltac values

7 files changed, 150 insertions, 112 deletions

diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index 1a2d89586..fea9e837b 100644
--- a/plugins/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
@@ -155,6 +155,4 @@ let () =
   | None -> mt ()
   | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic tac
   in
-  (* should not happen *)
-  let dummy _ _ _ expr = assert false in
-  Pptactic.declare_extra_genarg_pprule wit_withtac printer dummy dummy
+  Pptactic.declare_extra_vernac_genarg_pprule wit_withtac printer
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index c22e68323..b148d962e 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -195,8 +195,7 @@ let binders = Pcoq.create_generic_entry Pcoq.utactic "binders" (Genarg.rawwit wi
 
 let () =
   let raw_printer _ _ _ l = Pp.pr_non_empty_arg Ppconstr.pr_binders l in
-  let printer _ _ _ _ = Pp.str "<Unavailable printer for binders>" in
-  Pptactic.declare_extra_genarg_pprule wit_binders raw_printer printer printer
+  Pptactic.declare_extra_vernac_genarg_pprule wit_binders raw_printer
 
 open Pcoq
 
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index d588c888c..e467d3e2c 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -116,7 +116,13 @@ type 'a extra_genarg_printer =
         | Val.Base t ->
           begin match Val.eq t tag with
           | None -> default
-          | Some Refl -> Genprint.generic_top_print (in_gen (Topwit wit) x)
+          | Some Refl ->
+             let open Genprint in
+             match generic_top_print (in_gen (Topwit wit) x) with
+             | PrinterBasic pr -> pr ()
+             | PrinterNeedsContext pr -> pr (Global.env()) Evd.empty
+             | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+                printer (Global.env()) Evd.empty default_ensure_surrounded
           end
         | _ -> default
 
@@ -432,12 +438,13 @@ type 'a extra_genarg_printer =
       let pr_occs = pr_with_occurrences (fun () -> str" |- *") (occs,()) in
       (prlist_with_sep (fun () -> str", ") (pr_hyp_location pr_id) l ++ pr_occs)
 
-  let pr_clauses default_is_concl pr_id = function
+  (* Some true = default is concl; Some false = default is all; None = no default *)
+  let pr_clauses has_default pr_id = function
     | { onhyps=Some []; concl_occs=occs }
-        when (match default_is_concl with Some true -> true | _ -> false) ->
+        when (match has_default with Some true -> true | _ -> false) ->
       pr_with_occurrences mt (occs,())
     | { onhyps=None; concl_occs=AllOccurrences }
-        when (match default_is_concl with Some false -> true | _ -> false) -> mt ()
+        when (match has_default with Some false -> true | _ -> false) -> mt ()
     | { onhyps=None; concl_occs=NoOccurrences } ->
       pr_in (str " * |-")
     | { onhyps=None; concl_occs=occs } ->
@@ -1174,83 +1181,122 @@ let declare_extra_genarg_pprule wit
     g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) x
   in
   let h x =
-    let env = Global.env () in
-    h (pr_econstr_env env Evd.empty) (pr_leconstr_env env Evd.empty) (fun _ _ -> str "<tactic>") x
+    Genprint.PrinterNeedsContext (fun env sigma ->
+        h (pr_econstr_env env sigma) (pr_leconstr_env env sigma) (fun _ _ -> str "<tactic>") x)
   in
   Genprint.register_print0 wit f g h
 
+let declare_extra_vernac_genarg_pprule wit f =
+  let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in
+  Genprint.register_vernac_print0 wit f
+
 (** Registering *)
 
-let run_delayed c = c (Global.env ()) Evd.empty
+let pr_intro_pattern_env p = Genprint.PrinterNeedsContext (fun env sigma ->
+  let print_constr c = let (sigma, c) = c env sigma in pr_econstr_env env sigma c in
+  Miscprint.pr_intro_pattern print_constr p)
+
+let pr_red_expr_env r = Genprint.PrinterNeedsContext (fun env sigma ->
+  pr_red_expr (pr_econstr_env env sigma, pr_leconstr_env env sigma,
+               pr_evaluable_reference_env env, pr_constr_pattern_env env sigma) r)
+
+let pr_bindings_env bl = Genprint.PrinterNeedsContext (fun env sigma ->
+  let sigma, bl = bl env sigma in
+  Miscprint.pr_bindings
+    (pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl)
+
+let pr_with_bindings_env bl = Genprint.PrinterNeedsContext (fun env sigma ->
+  let sigma, bl = bl env sigma in
+  pr_with_bindings
+    (pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl)
+
+let pr_destruction_arg_env c = Genprint.PrinterNeedsContext (fun env sigma ->
+  let sigma, c = match c with
+  | clear_flag,ElimOnConstr g -> let sigma,c = g env sigma in sigma,(clear_flag,ElimOnConstr c)
+  | clear_flag,ElimOnAnonHyp n as x -> sigma, x
+  | clear_flag,ElimOnIdent id as x -> sigma, x in
+  pr_destruction_arg
+    (pr_econstr_env env sigma) (pr_leconstr_env env sigma) c)
+
+let make_constr_printer f c =
+  Genprint.PrinterNeedsContextAndLevel {
+      Genprint.default_already_surrounded = Ppconstr.ltop;
+      Genprint.default_ensure_surrounded = Ppconstr.lsimpleconstr;
+      Genprint.printer = (fun env sigma n -> f env sigma n c)}
 
-let run_delayed_destruction_arg = function (* HH: Using Evd.empty looks suspicious *)
-  | clear_flag,ElimOnConstr g -> clear_flag,ElimOnConstr (snd (run_delayed g))
-  | clear_flag,ElimOnAnonHyp n as x -> x
-  | clear_flag,ElimOnIdent id as x -> x
+let lift f a = Genprint.PrinterBasic (fun () -> f a)
 
 let () =
   let pr_bool b = if b then str "true" else str "false" in
   let pr_unit _ = str "()" in
-  let pr_string s = str "\"" ++ str s ++ str "\"" in
   Genprint.register_print0 wit_int_or_var
-    (pr_or_var int) (pr_or_var int) int;
+    (pr_or_var int) (pr_or_var int) (lift int);
   Genprint.register_print0 wit_ref
-    pr_reference (pr_or_var (pr_located pr_global)) pr_global;
+    pr_reference (pr_or_var (pr_located pr_global)) (lift pr_global);
   Genprint.register_print0 wit_ident
-    pr_id pr_id pr_id;
+    pr_id pr_id (lift pr_id);
   Genprint.register_print0 wit_var
-    (pr_located pr_id) (pr_located pr_id) pr_id;
+    (pr_located pr_id) (pr_located pr_id) (lift pr_id);
   Genprint.register_print0
     wit_intro_pattern
     (Miscprint.pr_intro_pattern pr_constr_expr)
     (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c))
-    (Miscprint.pr_intro_pattern (fun c -> pr_econstr (snd (run_delayed c))));
+    pr_intro_pattern_env;
   Genprint.register_print0
     wit_clause_dft_concl
     (pr_clauses (Some true) pr_lident)
     (pr_clauses (Some true) pr_lident)
-    (pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)))
+    (fun c -> Genprint.PrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)) c))
   ;
   Genprint.register_print0
     wit_constr
     Ppconstr.pr_constr_expr
     (fun (c, _) -> Printer.pr_glob_constr c)
-    Printer.pr_econstr
+    (make_constr_printer Printer.pr_econstr_n_env)
   ;
   Genprint.register_print0
     wit_uconstr
     Ppconstr.pr_constr_expr
     (fun (c,_) -> Printer.pr_glob_constr c)
-    Printer.pr_closed_glob
+    (make_constr_printer Printer.pr_closed_glob_n_env)
   ;
   Genprint.register_print0
     wit_open_constr
     Ppconstr.pr_constr_expr
     (fun (c, _) -> Printer.pr_glob_constr c)
-    Printer.pr_econstr
+    (make_constr_printer Printer.pr_econstr_n_env)
   ;
   Genprint.register_print0 wit_red_expr
     (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr))
     (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_and_constr_expr pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr))
-    (pr_red_expr (pr_econstr, pr_leconstr, pr_evaluable_reference, pr_constr_pattern));
-  Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis;
+    pr_red_expr_env
+  ;
+  Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis (lift pr_quantified_hypothesis);
   Genprint.register_print0 wit_bindings
     (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr)
     (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
-    (fun it -> Miscprint.pr_bindings_no_with pr_econstr pr_leconstr (snd (run_delayed it)));
+    pr_bindings_env
+  ;
   Genprint.register_print0 wit_constr_with_bindings
     (pr_with_bindings pr_constr_expr pr_lconstr_expr)
     (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
-    (fun it -> pr_with_bindings pr_econstr pr_leconstr (snd (run_delayed it)));
+    pr_with_bindings_env
+  ;
+  Genprint.register_print0 wit_open_constr_with_bindings
+    (pr_with_bindings pr_constr_expr pr_lconstr_expr)
+    (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
+    pr_with_bindings_env
+  ;
   Genprint.register_print0 Tacarg.wit_destruction_arg
     (pr_destruction_arg pr_constr_expr pr_lconstr_expr)
     (pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
-    (fun it -> pr_destruction_arg pr_econstr pr_leconstr (run_delayed_destruction_arg it));
-  Genprint.register_print0 Stdarg.wit_int int int int;
-  Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool;
-  Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit;
-  Genprint.register_print0 Stdarg.wit_pre_ident str str str;
-  Genprint.register_print0 Stdarg.wit_string pr_string pr_string pr_string
+    pr_destruction_arg_env
+  ;
+  Genprint.register_print0 Stdarg.wit_int int int (lift int);
+  Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool (lift pr_bool);
+  Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit (lift pr_unit);
+  Genprint.register_print0 Stdarg.wit_pre_ident str str (lift str);
+  Genprint.register_print0 Stdarg.wit_string qstring qstring (lift qstring)
 
 let () =
   let printer _ _ prtac = prtac (0, E) in
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index d9da954fe..5ecfaf590 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -46,6 +46,10 @@ val declare_extra_genarg_pprule :
   'b glob_extra_genarg_printer ->
   'c extra_genarg_printer -> unit
 
+val declare_extra_vernac_genarg_pprule :
+  ('a, 'b, 'c) genarg_type ->
+  'a raw_extra_genarg_printer -> unit
+
 type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list
 
 type pp_tactic = {
@@ -69,11 +73,16 @@ val pr_may_eval :
 val pr_and_short_name : ('a -> Pp.t) -> 'a and_short_name -> Pp.t
 val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t
 
+val pr_evaluable_reference_env : env -> evaluable_global_reference -> Pp.t
+
+val pr_quantified_hypothesis : quantified_hypothesis -> Pp.t
+
 val pr_in_clause :
   ('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t
 
-val pr_clauses :  bool option ->
+val pr_clauses : (* default: *) bool option ->
   ('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t
+  (* Some true = default is concl; Some false = default is all; None = no default *)
 
 val pr_raw_generic : env -> rlevel generic_argument -> Pp.t
 
@@ -116,3 +125,6 @@ val pr_value : tolerability -> Val.t -> Pp.t
 
 
 val ltop : tolerability
+
+val make_constr_printer : (env -> Evd.evar_map -> Notation_term.tolerability -> 'a -> Pp.t) ->
+  'a Genprint.top_printer
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index a79a92a66..4d171ecbc 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -17,15 +17,23 @@ open Geninterp
 
 exception CannotCoerceTo of string
 
+let base_val_typ wit =
+  match val_tag (topwit wit) with Val.Base t -> t | _ -> CErrors.anomaly (Pp.str "Not a base val.")
+
 let (wit_constr_context : (Empty.t, Empty.t, EConstr.constr) Genarg.genarg_type) =
   let wit = Genarg.create_arg "constr_context" in
   let () = register_val0 wit None in
+  let () = Genprint.register_val_print0 (base_val_typ wit)
+    (Pptactic.make_constr_printer Printer.pr_econstr_n_env) in
   wit
 
 (* includes idents known to be bound and references *)
 let (wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_binders) Genarg.genarg_type) =
   let wit = Genarg.create_arg "constr_under_binders" in
   let () = register_val0 wit None in
+  let () = Genprint.register_val_print0 (base_val_typ wit)
+             (fun c ->
+               Genprint.PrinterNeedsContext (fun env sigma -> Printer.pr_constr_under_binders_env env sigma c)) in
   wit
 
 (** All the types considered here are base types *)
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 0bf6e3d15..ee84be541 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -63,28 +63,37 @@ let get_separator = function
 | None -> user_err Pp.(str "Missing separator.")
 | Some sep -> sep
 
-let rec parse_user_entry s sep =
+let check_separator ?loc = function
+| None -> ()
+| Some _ -> user_err ?loc (str "Separator is only for arguments with suffix _list_sep.")
+
+let rec parse_user_entry ?loc s sep =
   let l = String.length s in
   if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
-    let entry = parse_user_entry (String.sub s 3 (l-8)) None in
+    let entry = parse_user_entry ?loc (String.sub s 3 (l-8)) None in
+    check_separator ?loc sep;
     Ulist1 entry
   else if l > 12 && coincide s "ne_" 0 &&
                    coincide s "_list_sep" (l-9) then
-    let entry = parse_user_entry (String.sub s 3 (l-12)) None in
+    let entry = parse_user_entry ?loc (String.sub s 3 (l-12)) None in
     Ulist1sep (entry, get_separator sep)
   else if l > 5 && coincide s "_list" (l-5) then
-    let entry = parse_user_entry (String.sub s 0 (l-5)) None in
+    let entry = parse_user_entry ?loc (String.sub s 0 (l-5)) None in
+    check_separator ?loc sep;
     Ulist0 entry
   else if l > 9 && coincide s "_list_sep" (l-9) then
-    let entry = parse_user_entry (String.sub s 0 (l-9)) None in
+    let entry = parse_user_entry ?loc (String.sub s 0 (l-9)) None in
     Ulist0sep (entry, get_separator sep)
   else if l > 4 && coincide s "_opt" (l-4) then
-    let entry = parse_user_entry (String.sub s 0 (l-4)) None in
+    let entry = parse_user_entry ?loc (String.sub s 0 (l-4)) None in
+    check_separator ?loc sep;
     Uopt entry
   else if Int.equal l 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then
     let n = Char.code s.[6] - 48 in
+    check_separator ?loc sep;
     Uentryl ("tactic", n)
   else
+    let _ = check_separator ?loc sep in
     Uentry s
 
 let interp_entry_name interp symb =
@@ -203,7 +212,7 @@ let register_tactic_notation_entry name entry =
 let interp_prod_item = function
   | TacTerm s -> TacTerm s
   | TacNonTerm (loc, ((nt, sep), ido)) ->
-    let symbol = parse_user_entry nt sep in
+    let symbol = parse_user_entry ?loc nt sep in
     let interp s = function
     | None ->
       if String.Map.mem s !entry_names then String.Map.find s !entry_names
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 66f124d2d..fd75862c6 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -76,6 +76,9 @@ let out_gen wit v =
 
 let val_tag wit = val_tag (topwit wit)
 
+let base_val_typ wit =
+  match val_tag wit with Val.Base t -> t | _ -> anomaly (str "Not a base val.")
+
 let pr_argument_type arg =
   let Val.Dyn (tag, _) = arg in
   Val.pr tag
@@ -124,6 +127,8 @@ type tacvalue =
 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
   wit
 
 let of_tacvalue v = in_gen (topwit wit_tacvalue) v
@@ -231,24 +236,16 @@ let curr_debug ist = match TacStore.get ist.extra f_debug with
 (* Displays a value *)
 let pr_value env v =
   let v = Value.normalize v in
-  if has_type v (topwit wit_tacvalue) then str "a tactic"
-  else if has_type v (topwit wit_constr_context) then
-    let c = out_gen (topwit wit_constr_context) v in
-    match env with
-    | Some (env,sigma) -> pr_leconstr_env env sigma c
-    | _ -> str "a term"
-  else if has_type v (topwit wit_constr) then
-    let c = out_gen (topwit wit_constr) v in
+  let pr_with_env pr =
     match env with
-    | Some (env,sigma) -> pr_leconstr_env env sigma c
-    | _ -> str "a term"
-  else if has_type v (topwit wit_constr_under_binders) then
-    let c = out_gen (topwit wit_constr_under_binders) v in
-    match env with
-    | Some (env,sigma) -> pr_lconstr_under_binders_env env sigma c
-    | _ -> str "a term"
-  else
-    str "a value of type" ++ spc () ++ pr_argument_type v
+    | Some (env,sigma) -> pr env sigma
+    | 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 } ->
+     pr_with_env (fun env sigma -> printer env sigma default_already_surrounded)
 
 let pr_closure env ist body =
   let pp_body = Pptactic.pr_glob_tactic env body in
@@ -818,51 +815,16 @@ let interp_constr_may_eval ist env sigma c =
   end
 
 (** TODO: should use dedicated printers *)
-let rec message_of_value v =
+let message_of_value v =
   let v = Value.normalize v in
-  let open Ftactic in
-  if has_type v (topwit wit_tacvalue) then
-    Ftactic.return (str "<tactic>")
-  else if has_type v (topwit wit_constr) then
-    let v = out_gen (topwit wit_constr) v in
-    Ftactic.enter begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) v) end
-  else if has_type v (topwit wit_constr_under_binders) then
-    let c = out_gen (topwit wit_constr_under_binders) v in
-    Ftactic.enter begin fun gl ->
-      Ftactic.return (pr_constr_under_binders_env (pf_env gl) (project gl) c)
-    end
-  else if has_type v (topwit wit_unit) then
-    Ftactic.return (str "()")
-  else if has_type v (topwit wit_int) then
-    Ftactic.return (int (out_gen (topwit wit_int) v))
-  else if has_type v (topwit wit_intro_pattern) then
-    let p = out_gen (topwit wit_intro_pattern) v in
-    let print env sigma c =
-      let (sigma, c) = c env sigma in
-      pr_econstr_env env sigma c
-    in
-    Ftactic.enter begin fun gl ->
-      Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (project gl) c) p)
-    end
-  else if has_type v (topwit wit_constr_context) then
-    let c = out_gen (topwit wit_constr_context) v in
-    Ftactic.enter begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) c) end
-  else if has_type v (topwit wit_uconstr) then
-    let c = out_gen (topwit wit_uconstr) v in
-    Ftactic.enter begin fun gl ->
-      Ftactic.return (pr_closed_glob_env (pf_env gl)
-                        (project gl) c)
-    end
-  else if has_type v (topwit wit_var) then
-    let id = out_gen (topwit wit_var) v in
-    Ftactic.enter begin fun gl -> Ftactic.return (Id.print id) end
-  else match Value.to_list v with
-  | Some l ->
-    Ftactic.List.map message_of_value l >>= fun l ->
-    Ftactic.return (prlist_with_sep spc (fun x -> x) l)
-  | None ->
-    let tag = pr_argument_type v in
-    Ftactic.return (str "<" ++ tag ++ str ">") (** TODO *)
+  let pr_with_env pr =
+    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 } ->
+     pr_with_env (fun env sigma -> printer env sigma default_ensure_surrounded)
 
 let interp_message_token ist = function
   | MsgString s -> Ftactic.return (str s)
@@ -946,13 +908,13 @@ let interp_in_hyp_as ist env sigma (id,ipat) =
   let sigma, ipat = interp_intro_pattern_option ist env sigma ipat in
   sigma,(interp_hyp ist env sigma id,ipat)
 
-let interp_binding_name ist sigma = function
+let interp_binding_name ist env sigma = function
   | AnonHyp n -> AnonHyp n
   | NamedHyp id ->
       (* If a name is bound, it has to be a quantified hypothesis *)
       (* user has to use other names for variables if these ones clash with *)
       (* a name intented to be used as a (non-variable) identifier *)
-      try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist None(Loc.tag id)
+      try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist (Some (env,sigma)) (Loc.tag id)
       with Not_found -> NamedHyp id
 
 let interp_declared_or_quantified_hypothesis ist env sigma = function
@@ -964,7 +926,7 @@ let interp_declared_or_quantified_hypothesis ist env sigma = function
 
 let interp_binding ist env sigma (loc,(b,c)) =
   let sigma, c = interp_open_constr ist env sigma c in
-  sigma, (loc,(interp_binding_name ist sigma b,c))
+  sigma, (loc,(interp_binding_name ist env sigma b,c))
 
 let interp_bindings ist env sigma = function
 | NoBindings ->
@@ -1386,10 +1348,14 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
         end >>= fun v ->
         (* No errors happened, we propagate the trace *)
         let v = append_trace trace v in
-        Proofview.tclLIFT begin
-          debugging_step ist
-	    (fun () ->
-	      str"evaluation returns"++fnl()++pr_value None v)
+        let call_debug env =
+          Proofview.tclLIFT (debugging_step ist (fun () -> str"evaluation returns"++fnl()++pr_value env v)) in
+        begin
+          let open Genprint in
+          match generic_val_print v with
+          | PrinterBasic _ -> call_debug None
+          | PrinterNeedsContext _ | PrinterNeedsContextAndLevel _ ->
+             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
       else