From 78d393576f3744f62115cbd3b26b484d5309031c Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Fri, 29 Jul 2022 16:04:09 +0200
Subject: [PATCH 1/3] fix location printing for string parsing

---
 src/coq_elpi_vernacular.ml | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml
index b45100ede..0e7298de3 100644
--- a/src/coq_elpi_vernacular.ml
+++ b/src/coq_elpi_vernacular.ml
@@ -51,30 +51,30 @@ let unit_from_file ~elpi x =
 let unit_from_string ~elpi loc x =
   try EC.unit ~elpi ~flags:(cc_flags ()) (EP.program_from ~elpi ~loc (Lexing.from_string x))
   with
-  | EP.ParseError(loc, msg) ->
+  | EP.ParseError(oloc, msg) ->
     let loc = Coq_elpi_utils.to_coq_loc loc in
-    CErrors.user_err ~loc (Pp.str msg)
+    CErrors.user_err ~loc Pp.(str (API.Ast.Loc.show oloc) ++ str msg)
   | EC.CompileError(oloc, msg) ->
     let loc = Option.map Coq_elpi_utils.to_coq_loc oloc in
-    CErrors.user_err ?loc (Pp.str msg)
+    CErrors.user_err ?loc Pp.(str (Option.default "" @@ Option.map API.Ast.Loc.show oloc) ++ str msg)
 
 let parse_goal ~elpi loc text =
   try EP.goal ~elpi ~loc ~text
-  with EP.ParseError(loc, msg) ->
-    let loc = Coq_elpi_utils.to_coq_loc loc in
-    CErrors.user_err ~loc (Pp.str msg)
+  with EP.ParseError(oloc, msg) ->
+    let loc = Coq_elpi_utils.to_coq_loc oloc in
+    CErrors.user_err ~loc Pp.(str (API.Ast.Loc.show oloc) ++ str msg)
 
 let assemble_units ~elpi units =
   try EC.assemble ~elpi ~flags:(cc_flags ()) units
   with EC.CompileError(oloc, msg) ->
     let loc = Option.map Coq_elpi_utils.to_coq_loc oloc in
-    CErrors.user_err ?loc (Pp.str msg)
+    CErrors.user_err ?loc Pp.(str (Option.default "" @@ Option.map API.Ast.Loc.show oloc) ++ str msg)
 
 let extend_w_units ~base units =
   try EC.extend ~flags:(cc_flags ()) ~base units
   with EC.CompileError(oloc, msg) ->
     let loc = Option.map Coq_elpi_utils.to_coq_loc oloc in
-    CErrors.user_err ?loc (Pp.str msg)
+    CErrors.user_err ?loc Pp.(str (Option.default "" @@ Option.map API.Ast.Loc.show oloc) ++ str msg)
 
 type program_name = Loc.t * qualified_name
 

From b36bfad8ba59848ce66328e4a7146bec4db332a0 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Sat, 30 Jul 2022 14:54:32 +0200
Subject: [PATCH 2/3] close changelog

---
 Changelog.md | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/Changelog.md b/Changelog.md
index a96ae198b..01b36ea32 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,5 +1,12 @@
 # Changelog
 
+## [1.15.5] - 30-07-2022
+
+Requires Elpi 1.16.5 and Coq 8.16.
+
+- Fix parse error location display for inline code
+- Fix HOAS of evars: pruning was not propagated to the type of the evar
+
 ## [1.15.4] - 26-07-2022
 
 Requires Elpi 1.16.5 and Coq 8.16.

From 0668e1b3733ae8238c7699db20289ea80bcfa1a5 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Sat, 30 Jul 2022 15:05:26 +0200
Subject: [PATCH 3/3] cleanup libobject (fix #253)

---
 _CoqProject.test           |  3 +++
 src/coq_elpi_vernacular.ml | 49 ++++++++++++++++++++++----------------
 tests/test_libobject_A.v   |  7 ++++++
 tests/test_libobject_B.v   | 13 ++++++++++
 tests/test_libobject_C.v   | 15 ++++++++++++
 5 files changed, 66 insertions(+), 21 deletions(-)
 create mode 100644 tests/test_libobject_A.v
 create mode 100644 tests/test_libobject_B.v
 create mode 100644 tests/test_libobject_C.v

diff --git a/_CoqProject.test b/_CoqProject.test
index 6e7d5ed50..9f0adf3b5 100644
--- a/_CoqProject.test
+++ b/_CoqProject.test
@@ -31,3 +31,6 @@ tests/test_COQ_ELPI_ATTRIBUTES.v
 tests/perf_calls.v
 tests/test_require_bad_order.v
 tests/test_ctx_cache.v
+tests/test_libobject_A.v
+tests/test_libobject_B.v
+tests/test_libobject_C.v
diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml
index 0e7298de3..fabfec1f2 100644
--- a/src/coq_elpi_vernacular.ml
+++ b/src/coq_elpi_vernacular.ml
@@ -295,7 +295,8 @@ let append_to_prog name nature l =
   seen, nature, prog
 
 let in_program : qualified_name * nature option * src list -> Libobject.obj =
-  Libobject.declare_object @@ Libobject.global_object_nodischarge "ELPI"
+  let open Libobject in
+  declare_object @@ global_object_nodischarge "ELPI"
     ~cache:(fun (name,nature,src_ast) ->
       program_src :=
         SLMap.add name (append_to_prog name nature src_ast) !program_src)
@@ -330,21 +331,22 @@ type snippet = {
 }
 
 let in_db : Names.Id.t -> snippet -> Libobject.obj =
+  let open Libobject in
   let cache ((_,kname), { program = name; code = p; _ }) =
     db_name_src := SLMap.add name (append_to_db name (kname,p)) !db_name_src in
   let import i (_, s as o) = if Int.equal i 1 || s.scope =  Coq_elpi_utils.SuperGlobal then cache o in
-  Libobject.declare_named_object @@ { (Libobject.default_object "ELPI-DB") with
-    Libobject.classify_function = (fun { scope; program; _ } ->
+  declare_named_object @@ { (default_object "ELPI-DB") with
+    classify_function = (fun { scope; program; _ } ->
       match scope with
-      | Coq_elpi_utils.Local -> Libobject.Dispose
-      | Coq_elpi_utils.Regular -> Libobject.Substitute
-      | Coq_elpi_utils.Global -> Libobject.Keep
-      | Coq_elpi_utils.SuperGlobal -> Libobject.Keep);
-    Libobject.load_function  = import;
-    Libobject.cache_function  = cache;
-    Libobject.subst_function = (fun (_,o) -> o);
-    Libobject.open_function = Libobject.simple_open import;
-    Libobject.discharge_function = (fun (({ scope; program; vars; } as o)) ->
+      | Coq_elpi_utils.Local -> Dispose
+      | Coq_elpi_utils.Regular -> Substitute
+      | Coq_elpi_utils.Global -> Keep
+      | Coq_elpi_utils.SuperGlobal -> Keep);
+    load_function  = import;
+    cache_function  = cache;
+    subst_function = (fun (_,o) -> o);
+    open_function = simple_open import;
+    discharge_function = (fun (({ scope; program; vars; } as o)) ->
       if scope = Coq_elpi_utils.Local || (List.exists (fun x -> Lib.is_in_section (Names.GlobRef.VarRef x)) vars) then None
       else Some o);
 
@@ -357,8 +359,9 @@ let add_to_db program code vars scope =
 
 let lp_command_ast = Summary.ref ~name:"elpi-lp-command" None
 let in_lp_command_src : src -> Libobject.obj =
-  Libobject.declare_object { Libobject.(default_object "ELPI-LP-COMMAND") with
-    Libobject.load_function = (fun _ x -> lp_command_ast := Some x);
+  let open Libobject in
+  declare_object { (default_object "ELPI-LP-COMMAND") with
+    load_function = (fun _ x -> lp_command_ast := Some x);
 }
 let load_command s =
   let elpi = ensure_initialized () in
@@ -375,8 +378,9 @@ let command_init () =
 
 let lp_tactic_ast = Summary.ref ~name:"elpi-lp-tactic" None
 let in_lp_tactic_ast : src -> Libobject.obj =
-  Libobject.declare_object { Libobject.(default_object "ELPI-LP-TACTIC") with
-    Libobject.load_function = (fun _ x -> lp_tactic_ast := Some x);
+  let open Libobject in
+  declare_object { (default_object "ELPI-LP-TACTIC") with
+    load_function = (fun _ x -> lp_tactic_ast := Some x);
 }
 let load_tactic s =
   let elpi = ensure_initialized () in
@@ -437,8 +441,9 @@ let get x =
 
 let lp_checker_ast = Summary.ref ~name:"elpi-lp-checker" None
 let in_lp_checker_ast : EC.compilation_unit list -> Libobject.obj =
-  Libobject.declare_object { Libobject.(default_object "ELPI-LP-CHECKER") with
-    Libobject.load_function = (fun _ x -> lp_checker_ast := Some x);
+  let open Libobject in
+  declare_object { (default_object "ELPI-LP-CHECKER") with
+    load_function = (fun _ x -> lp_checker_ast := Some x);
 }
 
 let load_checker s =
@@ -454,8 +459,9 @@ let checker () =
 
 let lp_printer_ast = Summary.ref ~name:"elpi-lp-printer" None
 let in_lp_printer_ast : EC.compilation_unit -> Libobject.obj =
-  Libobject.declare_object { Libobject.(default_object "ELPI-LP-PRINTER") with
-    Libobject.load_function = (fun _ x -> lp_printer_ast := Some x);
+  let open Libobject in
+  declare_object { (default_object "ELPI-LP-PRINTER") with
+    load_function = (fun _ x -> lp_printer_ast := Some x);
 }
 let load_printer s =
   let elpi = ensure_initialized () in
@@ -871,7 +877,8 @@ let subst_program = function
   | _, (Program _,_,_) -> assert false
 
 let in_exported_program : nature * qualified_name * string -> Libobject.obj =
-  Libobject.declare_object @@ Libobject.global_object_nodischarge "ELPI-EXPORTED"
+  let open Libobject in
+  declare_object @@ global_object_nodischarge "ELPI-EXPORTED"
     ~cache:cache_program
     ~subst:(Some subst_program)
 
diff --git a/tests/test_libobject_A.v b/tests/test_libobject_A.v
new file mode 100644
index 000000000..c5750f723
--- /dev/null
+++ b/tests/test_libobject_A.v
@@ -0,0 +1,7 @@
+From elpi Require Import elpi.
+
+Elpi Db a.db lp:{{
+  pred a o:term.
+  :name "init" a {{ 0 }}.
+  a {{ 1 }}.
+}}.
diff --git a/tests/test_libobject_B.v b/tests/test_libobject_B.v
new file mode 100644
index 000000000..65cd8af2e
--- /dev/null
+++ b/tests/test_libobject_B.v
@@ -0,0 +1,13 @@
+From elpi Require Import elpi.
+
+From elpi.tests Require Import test_libobject_A.
+
+Elpi Tactic tac.
+Elpi Accumulate Db a.db.
+Elpi Accumulate lp:{{
+  solve _ _ :-
+    a X, coq.say X.
+}}.
+Elpi Typecheck.
+
+Ltac b := elpi tac.
diff --git a/tests/test_libobject_C.v b/tests/test_libobject_C.v
new file mode 100644
index 000000000..30cee6ca5
--- /dev/null
+++ b/tests/test_libobject_C.v
@@ -0,0 +1,15 @@
+From elpi.tests Require Import test_libobject_B.
+
+Goal True.
+  b.
+Abort.
+
+Import elpi.
+
+Elpi Accumulate a.db lp:{{ 
+  :before "init" a {{ 3 }}.
+}}.
+
+Goal True.
+b.
+Abort.