From d5f07aa398419335ec84d609956e39330d8a6a77 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Wed, 21 Feb 2024 10:23:17 +0100
Subject: [PATCH 1/2] Update doc

---
 README.md | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/README.md b/README.md
index d6620a80c..f14bdab72 100644
--- a/README.md
+++ b/README.md
@@ -181,14 +181,13 @@ In order to load Coq-Elpi use `From elpi Require Import elpi`.
   It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands).
 - `Elpi Program <qname> <code>` lower level primitive letting one crate a
   command/tactic with a custom preamble `<code>`.
-
-- `Elpi Accumulate [<qname>] [<code>|File <filename> From <loadpath>|Db <dbname>]`
+- `From some.load.path Extra Dependency "filename" as <fname>`.
+- `Elpi Accumulate [<qname>] [<code>|File <fname>|Db <dbname>]`
   adds code to the current program (or `<qname>` if specified).
   The code can be verbatim, from a file or a Db.
   It understands the `#[skip="rex"]` and `#[only="rex"]` which make the command
   a no op if the Coq version is matched (or not) by the given regular expression.
-  File names are relative to the directory mapped to `<loadpath>`; if more than
-  one such directory exists, the `<filename>` must exists only once.
+  File names `<fname>` must have been previously declared with the above command.
   It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands)
 - `Elpi Typecheck [<qname>]` typechecks the current program (or `<qname>` if
   specified).

From f82bee7c604fb16dd46f4fa93d02ade2f6ac0b86 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Thu, 22 Feb 2024 09:31:50 +0100
Subject: [PATCH 2/2] ppgoal

---
 Changelog.md             |  5 +++++
 coq-builtin.elpi         | 10 ++++++++++
 src/coq_elpi_builtins.ml | 24 ++++++++++++++++++++++++
 tests/test_tactic.v      |  8 +++-----
 4 files changed, 42 insertions(+), 5 deletions(-)

diff --git a/Changelog.md b/Changelog.md
index 7c514f5ec..fbc605634 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,5 +1,10 @@
 # Changelog
 
+## UNRELEASED
+
+### API
+- New `coq.goal->pp`
+
 ## [2.0.2] - 01/02/2024
 
 Requires Elpi 1.18.2 and Coq 8.19.
diff --git a/coq-builtin.elpi b/coq-builtin.elpi
index d5a2085af..1e747a3b1 100644
--- a/coq-builtin.elpi
+++ b/coq-builtin.elpi
@@ -1691,6 +1691,16 @@ external pred coq.term->string i:term, o:string.
 % - @holes! (default: false, prints evars as _)
 external pred coq.term->pp i:term, o:coq.pp.
 
+% [coq.goal->pp G B] prints a goal G to a pp.t B using Coq's pretty
+% printer"
+% Supported attributes:
+% - @ppall! (default: false, prints all details)
+% - @ppmost! (default: false, prints most details)
+% - @pplevel! (default: _, prints parentheses to reach that level, 200 =
+% off)
+% - @holes! (default: false, prints evars as _)
+external pred coq.goal->pp i:goal, o:coq.pp.
+
 % -- Extra Dependencies -----------------------------------------------
 
 % [coq.extra-dep Identifier FileName] Resolve the file name of an extra
diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index 042f1d276..e675cbd02 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -3830,6 +3830,30 @@ Supported attributes:
      state, !: s, [])),
   DocAbove);
 
+  MLCode(Pred("coq.goal->pp",
+    CIn(goal,"G",
+    Out(ppboxes, "B",
+    Full(raw_ctx, {|prints a goal G to a pp.t B using Coq's pretty printer"
+Supported attributes:
+- @ppall! (default: false, prints all details)
+- @ppmost! (default: false, prints most details)
+- @pplevel! (default: _, prints parentheses to reach that level, 200 = off)
+- @holes! (default: false, prints evars as _)|}))),
+  (fun (proof_context,evar,args) _ ~depth _ _ state ->
+     let sigma = get_sigma state in
+     let pr_named_context_of env sigma =
+      let make_decl_list env d pps = Printer.pr_named_decl env sigma d :: pps in
+      let psl = List.rev (Environ.fold_named_context make_decl_list env ~init:[]) in
+      Pp.(v 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl)) in
+     let s = Pp.(repr @@ with_pp_options proof_context.options.pp (fun () ->
+        v 0 @@ 
+        pr_named_context_of proof_context.env sigma ++ cut () ++
+        str "======================" ++ cut () ++
+        Printer.pr_econstr_env proof_context.env sigma
+          Evd.(evar_concl @@ find_undefined sigma evar))) in
+     state, !: s, [])),
+  DocAbove);
+
   LPDoc "-- Extra Dependencies -----------------------------------------------";
 
   MLCode(Pred("coq.extra-dep",
diff --git a/tests/test_tactic.v b/tests/test_tactic.v
index fb88cf908..26e939e97 100644
--- a/tests/test_tactic.v
+++ b/tests/test_tactic.v
@@ -26,12 +26,10 @@ Elpi Print foobar.
 Elpi Tactic print_goal.
 Elpi Accumulate lp:{{
 
-  solve (goal L _ T _ As as G) [seal G] :-
+  solve (goal _ _ _ _ _ as G) [seal G] :-
     print_constraints,
-    coq.say "Goal: ", coq.say As, coq.say "\n",
-    coq.say L,
-    coq.say "------------",
-    coq.say T {coq.term->string T}.
+    coq.say "Goal: \n",
+    coq.say {coq.pp->string {coq.goal->pp G} }.
 
 }}.