From 565a9a1b5368c586e529fc9774e4cb4b81c6441b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 31 Oct 2017 17:18:50 +0100
Subject: Setting a system to register printers for Ltac values.

The model provides three kinds of printers depending on whether the
printer needs a context, and, if yes if it supports levels. In the
latter case, it takes defaults levels for printing when in a
surrounded context (lconstr style) and for printing when not in a
surrounded context (constr style).

This model preserves the 8.7 focussing semantics of "idtac"
(i.e. focussing only when an env is needed) but it also shows that the
semantics of "idtac", which focusses the goal depending on the type of
its arguments, is a bit ad hoc to understand.

See discussion at PR#6047
"https://github.com/coq/coq/pull/6047#discussion_r148278454".
---
 plugins/ltac/taccoerce.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'plugins/ltac/taccoerce.ml')

diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index a79a92a661..4d171ecbc2 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 *)
-- 
cgit v1.2.3