Merge PR coq#18472: Add debug printer for goal_with_state

Reviewed-by: ppedrot Co-authored-by: ppedrot <[email protected]>
Villetaneuse · Jan 10, 2024 · db93e18 · db93e18
2 parents b7f2ed5 + fedb8fc
commit db93e18
Show file tree

Hide file tree

Showing 4 changed files with 4 additions and 0 deletions.
diff --git a/dev/include_printers b/dev/include_printers
@@ -34,6 +34,7 @@
 (*#install_printer  (* hint_db *)  print_hint_db;;*)
 (*#install_printer  (* hints_path *)  pphintspath;;*)
 #install_printer  (* goal *)  ppgoal;;
+#install_printer  ppgoal_with_state;;
 (*#install_printer  (* sigma goal *)  ppsigmagoal;;*)
 #install_printer  (* proof *)  pproof;;
 #install_printer  (* proofview *)  ppproofview;;

diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg
@@ -61,6 +61,7 @@ install_printer Top_printers.ppexistentialset
 install_printer Top_printers.ppexistentialfilter
 install_printer Top_printers.ppclenv
 install_printer Top_printers.ppgoal
+install_printer Top_printers.ppgoal_with_state
 install_printer Top_printers.pphintdb
 install_printer Top_printers.ppproofview
 install_printer Top_printers.ppopenconstr

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
@@ -230,6 +230,7 @@ let ppexistentialfilter filter = match Evd.Filter.repr filter with
 let pr_goal e = Pp.(str "GOAL:" ++ int (Evar.repr e))
 let ppclenv clenv = pp(pr_clenv clenv)
 let ppgoal g = pp(Printer.Debug.pr_goal g)
+let ppgoal_with_state g = ppevar (Proofview_monad.drop_state g)
 let pphintdb db = pp(envpp Hints.pr_hint_db_env db)
 let ppproofview p =
   let gls,sigma = Proofview.proofview p in

diff --git a/dev/top_printers.mli b/dev/top_printers.mli
@@ -134,6 +134,7 @@ val ppexistentialfilter : Evd.Filter.t -> unit
 val ppclenv : Clenv.clausenv -> unit
 
 val ppgoal : Proofview.Goal.t -> unit
+val ppgoal_with_state : Proofview_monad.goal_with_state -> unit
 
 val pphintdb : Hints.Hint_db.t -> unit
 val ppproofview : Proofview.proofview -> unit