From be04179c148357edea49aded3cbcf8ff5527259c Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Mon, 8 Jan 2024 16:36:46 +0100
Subject: [PATCH 1/3] avoid declaring options twice

This can happen in a coq instance handling multiple files, eg vscoq
---
 apps/tc/theories/tc.v | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v
index 3b255f23d..0ba466e48 100644
--- a/apps/tc/theories/tc.v
+++ b/apps/tc/theories/tc.v
@@ -42,8 +42,10 @@ Elpi Accumulate File solver.
 Elpi Query lp:{{
   sigma Options\ 
     all-options Options,
-    std.forall Options (x\ sigma L\ x L, 
-      coq.option.add L (coq.option.bool ff) ff).
+    std.forall Options (x\ sigma L\ x L,
+      if (coq.option.available? L _)
+         true
+         (coq.option.add L (coq.option.bool ff) ff)).
 }}.
 Elpi Typecheck.
 

From d293ed7c6f82eecc40e9fb4a11884a14684ffd06 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Mon, 8 Jan 2024 17:14:12 +0100
Subject: [PATCH 2/3] fix: arg HOAS for definitional classes

---
 src/coq_elpi_arg_HOAS.ml | 2 ++
 tests/test_arg_HOAS.v    | 6 ++++++
 2 files changed, 8 insertions(+)

diff --git a/src/coq_elpi_arg_HOAS.ml b/src/coq_elpi_arg_HOAS.ml
index ab8e695bf..1121c6126 100644
--- a/src/coq_elpi_arg_HOAS.ml
+++ b/src/coq_elpi_arg_HOAS.ml
@@ -960,6 +960,8 @@ let in_elpi_cmd ~depth ?calldepth coq_ctx state ~raw (x : Cmd.top) =
       let open Vernacentries.Preprocessed_Mind_decl in
       let { flags = { template; poly; cumulative; udecl; finite }; primitive_proj; kind; records } = raw_rdecl in
       let template = handle_template_polymorphism template in
+      (* Definitional type classes cannot be interpreted using this function (why?) *)
+      let kind = if kind = Vernacexpr.Class true then Vernacexpr.Class false else kind in
       let e = Record.interp_structure ~template udecl kind ~cumulative ~poly ~primitive_proj finite records in
       record_entry2lp ~depth coq_ctx E.no_constraints state ~loose_udecl:(udecl = None) e
   | IndtDecl (_ist,(glob_sign,raw_indt)) when raw ->
diff --git a/tests/test_arg_HOAS.v b/tests/test_arg_HOAS.v
index 7f6527744..1ebae847a 100644
--- a/tests/test_arg_HOAS.v
+++ b/tests/test_arg_HOAS.v
@@ -245,6 +245,12 @@ End full_definition.
 
 (*****************************************)
 
+Module classes.
+Elpi declarations Class foo := bar : True.
+End classes.
+
+(*****************************************)
+
 Module copy.
 Import inductive_nup.
 

From 08a6554b3259890a54e09d24a034828beac6cd36 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Mon, 8 Jan 2024 17:43:12 +0100
Subject: [PATCH 3/3] fix glob quotation of section variables

---
 src/coq_elpi_glob_quotation.ml | 18 +++++++++++-------
 tests/test_quotation.v         | 11 +++++++++++
 2 files changed, 22 insertions(+), 7 deletions(-)

diff --git a/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml
index a82dc98e2..62bc3c0e1 100644
--- a/src/coq_elpi_glob_quotation.ml
+++ b/src/coq_elpi_glob_quotation.ml
@@ -59,18 +59,22 @@ let is_restricted_name =
   fun s -> Str.(string_match rex (Id.to_string s) 0)
 
 
-let glob_environment : Environ.env S.component =
+let glob_environment : Environ.env option S.component =
   S.declare_component ~name:"coq-elpi:glob-environment" ~descriptor:interp_state
-    ~pp:(fun _ _ -> ()) ~init:(fun () -> Global.env ())
-                        ~start:(fun _ -> Global.env ()) ()
+    ~pp:(fun _ _ -> ()) ~init:(fun () -> None)
+                        ~start:(fun _ -> Some (Global.env ())) ()
+
+(* Since Accumulate runs before the interpreter starts, the state
+   may be empty: ~start not called, ~init called too early *)
+let ensure_some f = function None -> Some (f (Global.env ())) | Some x -> Some (f x)
 
 let push_env state name =
   let open Context.Rel.Declaration in
-  S.update glob_environment state (Environ.push_rel (LocalAssum(Context.make_annot name Sorts.Relevant,Constr.mkProp)))
+  S.update glob_environment state (ensure_some (Environ.push_rel (LocalAssum(Context.make_annot name Sorts.Relevant,Constr.mkProp))))
 let pop_env state =
-  S.update glob_environment state (Environ.pop_rel_context 1)
+  S.update glob_environment state (ensure_some (Environ.pop_rel_context 1))
   
-let get_glob_env state = S.get glob_environment state
+let get_glob_env state = Option.get @@ ensure_some (fun x -> x) @@ S.get glob_environment state
 
 (* XXX: I don't get why we use a coq_ctx here *)
 let under_ctx name ty bo gterm2lp ~depth state x =
@@ -396,7 +400,7 @@ let coq_quotation ~depth state loc src =
       Constrintern.intern_constr (get_glob_env state) (get_sigma state) ce
     with e ->
       CErrors.user_err
-        Pp.(str(API.Ast.Loc.show loc) ++str":" ++ spc() ++ CErrors.print_no_report e)
+        Pp.(str(API.Ast.Loc.show loc) ++ spc() ++ CErrors.print_no_report e)
   in
   gterm2lp ~depth state glob
       
diff --git a/tests/test_quotation.v b/tests/test_quotation.v
index dfdd0efc3..cbe8746eb 100644
--- a/tests/test_quotation.v
+++ b/tests/test_quotation.v
@@ -83,3 +83,14 @@ Fail Elpi Query lp:{{ std.do! [
   std.assert-ok! (coq.typecheck T _) "does not typecheck",
 ]
 }}.
+
+Section A.
+Variable A : Type.
+Check 1.
+Elpi Accumulate lp:{{
+
+pred p i:term.
+p {{ A }}.
+
+}}.
+End A.
\ No newline at end of file