From 0ec84428d92703abfa92424fb84dfdd8ce0bc45a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Fri, 12 Jun 2020 17:32:55 +0200
Subject: [PATCH 01/22] [coq] disable memory hog tests

---
 theories/derive/tests/test_bcongr.v    | 4 ++--
 theories/derive/tests/test_eqK.v       | 4 ++--
 theories/derive/tests/test_eqOK.v      | 4 ++--
 theories/derive/tests/test_eqcorrect.v | 4 ++--
 4 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/theories/derive/tests/test_bcongr.v b/theories/derive/tests/test_bcongr.v
index 37dba5573..fcfaf52aa 100644
--- a/theories/derive/tests/test_bcongr.v
+++ b/theories/derive/tests/test_bcongr.v
@@ -20,7 +20,7 @@ Fail Elpi derive.bcongr dyn.
 Elpi derive.bcongr zeta.
 Elpi derive.bcongr beta.
 Fail Elpi derive.bcongr iota.
-Elpi derive.bcongr large.
+(* Elpi derive.bcongr large. *)
 End Coverage.
 
 Import Coverage.
@@ -60,4 +60,4 @@ Check beta_bcongr_Redex : forall A x y b, reflect (x = y) b -> reflect (Redex A
 
 Fail Check iota_bcongr_Why.
 
-Check large_bcongr_K1.
+(* Check large_bcongr_K1. *)
diff --git a/theories/derive/tests/test_eqK.v b/theories/derive/tests/test_eqK.v
index 5a5510eeb..90f08f0c6 100644
--- a/theories/derive/tests/test_eqK.v
+++ b/theories/derive/tests/test_eqK.v
@@ -28,7 +28,7 @@ Fail Elpi derive.eqK dyn.
 Elpi derive.eqK zeta.
 Elpi derive.eqK beta.
 Fail Elpi derive.eqK iota.
-Elpi derive.eqK large.
+(*Elpi derive.eqK large.*)
 
 End Coverage.
 
@@ -55,4 +55,4 @@ Check eq_axiom_Envelope.
 
 Check eq_axiom_Redex.
 
-Check eq_axiom_K1.
\ No newline at end of file
+(*Check eq_axiom_K1.*)
\ No newline at end of file
diff --git a/theories/derive/tests/test_eqOK.v b/theories/derive/tests/test_eqOK.v
index 0bd98972b..0d17772ac 100644
--- a/theories/derive/tests/test_eqOK.v
+++ b/theories/derive/tests/test_eqOK.v
@@ -24,7 +24,7 @@ Fail Elpi derive.eqOK dyn.
 Elpi derive.eqOK zeta.
 Elpi derive.eqOK beta.
 Fail Elpi derive.eqOK iota.
-Elpi derive.eqOK large.
+(* Elpi derive.eqOK large. *)
 End Coverage.
 
 Import Coverage.
@@ -45,7 +45,7 @@ Fail Check dyn_eq_OK.
 Check zeta_eq_OK : forall A f, ok A f -> ok (zeta A) (zeta_eq A f).
 Check beta_eq_OK : forall A f, ok A f -> ok (beta A) (beta_eq A f).
 Fail Check iota_eq_OK.
-Check large_eq_OK : ok large large_eq.
+(* Check large_eq_OK : ok large large_eq. *)
 
 From elpi Require Import test_param1_functor.
 Import test_param1_functor.Coverage.
diff --git a/theories/derive/tests/test_eqcorrect.v b/theories/derive/tests/test_eqcorrect.v
index 98ca2d2d8..ef68fadcd 100644
--- a/theories/derive/tests/test_eqcorrect.v
+++ b/theories/derive/tests/test_eqcorrect.v
@@ -26,7 +26,7 @@ Fail Elpi derive.eqcorrect dyn.
 Elpi derive.eqcorrect zeta.
 Elpi derive.eqcorrect beta.
 Fail Elpi derive.eqcorrect iota.
-Elpi derive.eqcorrect large.
+(* Elpi derive.eqcorrect large. *)
 End Coverage.
 
 Import Coverage.
@@ -47,5 +47,5 @@ Fail Check dyn_eq_correct.
 Check zeta_eq_correct : forall A f, correct (zeta A) (is_zeta A (eq_axiom_at A f)) (zeta_eq A f).
 Check beta_eq_correct : forall A f, correct (beta A) (is_beta A (eq_axiom_at A f)) (beta_eq A f).
 Fail Check iota_eq_correct.
-Check large_eq_correct : correct large is_large large_eq.
+(* Check large_eq_correct : correct large is_large large_eq. *)
 

From 778dccbd2a0e0a78b8348fa0795995973795e9f5 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Wed, 24 Jun 2020 13:49:01 +0200
Subject: [PATCH 02/22] [coq] Adapt to coq/coq#12372

---
 src/coq_elpi_builtins.ml | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index 173873ea0..cd334c1c5 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -956,7 +956,7 @@ It undestands qualified names, e.g. "Nat.t". It's a fatal error if Name cannot b
            ComAssumption.declare_variable false ~kind (EConstr.to_constr sigma ty) impargs Glob_term.Explicit variable;
            GlobRef.VarRef(Id.of_string id), Univ.Instance.empty
          end else
-           ComAssumption.declare_axiom false ~local:Declare.ImportDefaultBehavior ~poly:false ~kind (EConstr.to_constr sigma ty)
+           ComAssumption.declare_axiom false ~local:Locality.ImportDefaultBehavior ~poly:false ~kind (EConstr.to_constr sigma ty)
              (uentry, ubinders) impargs Declaremods.NoInline
              variable
        in
@@ -970,12 +970,11 @@ It undestands qualified names, e.g. "Nat.t". It's a fatal error if Name cannot b
        let udecl = UState.default_univ_decl in
        let kind = Decls.(IsDefinition Definition) in
        let scope = if local
-         then Declare.Discharge
-         else Declare.Global Declare.ImportDefaultBehavior in
-       let gr = DeclareDef.declare_definition
-           ~name:(Id.of_string id) ~scope ~kind ~impargs:[]
-           ~poly:false ~udecl ~opaque:(opaque = Given true) ~types ~body sigma
-       in
+         then Locality.Discharge
+         else Locality.(Global ImportDefaultBehavior) in
+       let cinfo = Declare.CInfo.make ~name:(Id.of_string id) ~typ:types ~impargs:[] () in
+       let info = Declare.Info.make ~scope ~kind ~poly:false ~udecl () in
+       let gr = Declare.declare_definition ~cinfo ~info ~opaque:(opaque = Given true) ~body sigma in
        state, !: (global_constant_of_globref gr), []))),
   DocAbove);
 

From ccf2a6caa8ad0d9907664661f41c8d05226e49c3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Fri, 14 Feb 2020 14:33:13 +0100
Subject: [PATCH 03/22] Adapt to coq/coq#10390 (UIP in SProp)

---
 src/coq_elpi_HOAS.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml
index f0e874584..a57e0e856 100644
--- a/src/coq_elpi_HOAS.ml
+++ b/src/coq_elpi_HOAS.ml
@@ -653,7 +653,7 @@ let rec constr2lp coq_ctx ~calldepth ~depth state t =
          check_univ_inst (EC.EInstance.kind sigma i);
          state, in_elpi_gr ~depth state (G.ConstructRef construct)
     | C.Case((*{ C.ci_ind; C.ci_npar; C.ci_cstr_ndecls; C.ci_cstr_nargs }*)_,
-             rt,t,bs) ->
+             rt,_,t,bs) ->
          let state, t = aux ~depth state t in
          let state, rt = aux ~depth state rt in
          let state, bs = CArray.fold_left_map (aux ~depth) state bs in
@@ -1006,7 +1006,7 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals
           aux rt None in
       let ci =
         Inductiveops.make_case_info (get_global_env state) ind Sorts.Relevant C.RegularStyle in
-      state, EC.mkCase (ci,rt,t,Array.of_list bt), gl1 @ gl2 @ gl3
+      state, EC.mkCase (ci,rt,C.NoInvert,t,Array.of_list bt), gl1 @ gl2 @ gl3
 
  (* fix *)
   | E.App(c,name,[rno;ty;bo]) when fixc == c ->

From 5bf6c311529d11d7a3bbadb4945101036f1c2fa2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maxime=20D=C3=A9n=C3=A8s?= <maxime.denes@inria.fr>
Date: Sun, 5 Jul 2020 13:31:45 +0200
Subject: [PATCH 04/22] Adapt to https://github.com/coq/coq/pull/11604

---
 src/coq_elpi_HOAS.ml           | 1 +
 src/coq_elpi_glob_quotation.ml | 1 +
 2 files changed, 2 insertions(+)

diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml
index a57e0e856..61eb5260e 100644
--- a/src/coq_elpi_HOAS.ml
+++ b/src/coq_elpi_HOAS.ml
@@ -669,6 +669,7 @@ let rec constr2lp coq_ctx ~calldepth ~depth state t =
     | C.Proj _ -> nYI "HOAS for primitive projections"
     | C.Int _ -> nYI "HOAS for primitive machine integers"
     | C.Float _ -> nYI "HOAS for primitive machine floats"
+    | C.Array _ -> nYI "HOAS for persistent arrays"
   in
   if debug () then
     Feedback.msg_debug Pp.(str"term2lp: depth=" ++ int depth ++
diff --git a/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml
index 61965f27b..cd97bb38e 100644
--- a/src/coq_elpi_glob_quotation.ml
+++ b/src/coq_elpi_glob_quotation.ml
@@ -284,6 +284,7 @@ let rec gterm2lp ~depth state x =
   | GRec _ -> nYI "(glob)HOAS mutual/non-struct fix"
   | GInt _ -> nYI "(glob)HOAS primitive machine integers"
   | GFloat _ -> nYI "(glob)HOAS primitive machine floats"
+  | GArray _ -> nYI "(glob)HOAS persistent arrays"
 ;;
 
 let coq_quotation ~depth state _loc src =

From c0797b1da8fb8382a1c662aa6ef419423f5b0309 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Tue, 7 Jul 2020 12:16:25 +0200
Subject: [PATCH 05/22] Adapt to coq/coq#12650 (cleanup
 declare_structure_entry)

---
 src/coq_elpi_builtins.ml | 16 +++++++++++-----
 1 file changed, 11 insertions(+), 5 deletions(-)

diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index cd334c1c5..ddf5cfe95 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -997,19 +997,25 @@ It undestands qualified names, e.g. "Nat.t". It's a fatal error if Name cannot b
                { Record.pf_subclass = is_coercion ; pf_canonical = is_canonical })
              field_specs)) in
          let is_implicit = List.map (fun _ -> []) names in
-         let rsp = ind in
-         let cstr = (rsp,1) in
+         let cstr = (ind,1) in
          let open Entries in
          let k_ty = List.(hd (hd me.mind_entry_inds).mind_entry_lc) in
          let fields_as_relctx = Term.prod_assum k_ty in
          let kinds, sp_projs =
-           Record.declare_projections rsp ~kind:Decls.Definition
+           Record.declare_projections ind ~kind:Decls.Definition
              (Evd.univ_entry ~poly:false sigma)
              (Names.Id.of_string "record")
              flags is_implicit fields_as_relctx
          in
-         Record.declare_structure_entry
-           (cstr, List.rev kinds, List.rev sp_projs);
+         let npars = Inductiveops.inductive_nparams (Global.env()) ind in
+         let struc = {
+           Recordops.s_CONST = cstr;
+           s_PROJ = List.rev sp_projs;
+           s_PROJKIND = List.rev kinds;
+           s_EXPECTEDPARAM = npars;
+         }
+         in
+         Record.declare_structure_entry struc;
      end;
      state, !: ind, []))),
   DocAbove);

From 0c1113c2e985093b412fbb08a30c1d907304abbc Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 29 Jul 2020 13:59:08 +0200
Subject: [PATCH 06/22] fix opam

---
 coq-elpi.opam | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/coq-elpi.opam b/coq-elpi.opam
index e24f49693..6c9d733f7 100644
--- a/coq-elpi.opam
+++ b/coq-elpi.opam
@@ -12,7 +12,7 @@ build: [ make "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" ]
 install: [ make "install" "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" ]
 depends: [
   "elpi" {>= "1.11.0" & < "1.12.0~"}
-  "coq" {>= "8.12" & < "8.13~" }
+  "coq" {= "dev"}
   ]
 synopsis: "Elpi extension language for Coq"
 description: """

From a3897697640bd0fbb656405876264e73982bf474 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 29 Jul 2020 14:01:23 +0200
Subject: [PATCH 07/22] fix CI

---
 .github/workflows/main.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 5ed02bcb8..5b61879aa 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -8,7 +8,7 @@ on:
   push:
     branches: [ master ]
   pull_request:
-    branches: [ master ]
+    branches: [ master, coq-master ]
 
 jobs:
   build:
@@ -16,7 +16,7 @@ jobs:
     strategy:
       matrix:
         coq_version:
-          - '8.12'
+          - dev
         ocaml_version:
           - 'minimal'
     steps:

From 3fe218d60d5c205cb6fe4b038fe7dadb92212422 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Fri, 28 Aug 2020 15:29:33 +0200
Subject: [PATCH 08/22] Adapt to Coq PR#12875: passing also name of implicit
 arguments to set_implicits.

---
 src/coq_elpi_builtins.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index 3516d050b..6f765ed7d 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -1399,8 +1399,8 @@ Supported attributes:
   (fun gref imps ~depth {options} _ -> on_global_state "coq.arguments.set-implicit" (fun state ->
      let local = options.local <> Some false in
      let imps = imps |> List.(map (map (function
-       | Unspec -> Glob_term.Explicit
-       | Given x -> x))) in
+       | Unspec -> Anonymous, Glob_term.Explicit
+       | Given x -> Anonymous, x))) in
      Impargs.set_implicits local gref imps;
      state, (), []))),
   DocAbove);

From 2849f8dd8e781ffc1606af9eefffe7296ef2d9a5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Mon, 31 Aug 2020 14:45:46 +0200
Subject: [PATCH 09/22] Adapt to coq/coq#12892 (update_sigma_univs)

---
 src/coq_elpi_HOAS.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml
index 4bf1da0f0..9498b6e5f 100644
--- a/src/coq_elpi_HOAS.ml
+++ b/src/coq_elpi_HOAS.ml
@@ -438,8 +438,8 @@ let hack_UState_demote_global_univs_missin_API_in_811 env (uctx : UState.t) =
   (Obj.magic uctx : UState.t)
 
  let from_env_keep_univ_of_sigma env sigma0 =
-   let sigma = Evd.update_sigma_env sigma0 env in
-   let sigma = Evd.from_ctx (hack_UState_demote_global_univs_missin_API_in_811 env (Evd.evar_universe_context sigma)) in
+   let uctx = UState.update_sigma_univs (Evd.evar_universe_context sigma0) (Environ.universes env) in
+   let sigma = Evd.from_ctx (hack_UState_demote_global_univs_missin_API_in_811 env uctx) in
    from_env_sigma env sigma
  let init () = from_env (Global.env ())
 

From 09dfaf253029d7b36dbdee24cfc7a6eaa3b00913 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Mon, 20 Jul 2020 12:58:32 +0200
Subject: [PATCH 10/22] Adapt to coq/coq#12653 (syntax for cumulative
 inductives)

---
 src/coq_elpi_HOAS.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml
index 9498b6e5f..0070cc08d 100644
--- a/src/coq_elpi_HOAS.ml
+++ b/src/coq_elpi_HOAS.ml
@@ -2032,7 +2032,7 @@ let lp2inductive_entry ~depth coq_ctx constraints state t =
       mind_entry_inds = [oe];
       mind_entry_universes =
         Monomorphic_entry (Evd.universe_context_set sigma);
-      mind_entry_cumulative = false;
+      mind_entry_variance = None;
       mind_entry_private = None; }, i_impls, kimpls, List.(concat (rev gls_rev))
   in
 

From 9110bc186c42060ee7bc90c0264764a3326984e6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= <pierre-marie.pedrot@inria.fr>
Date: Mon, 28 Sep 2020 12:22:25 +0200
Subject: [PATCH 11/22] Adapt w.r.t. coq/coq#13106.

---
 src/coq_elpi_vernacular.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml
index d752bb52d..47470f672 100644
--- a/src/coq_elpi_vernacular.ml
+++ b/src/coq_elpi_vernacular.ml
@@ -157,7 +157,6 @@ let intern_record_decl glob_sign { name; sort; parameters; constructor; fields }
     | Vernacexpr.AssumExpr ({ CAst.v = name } as fn,x), { Vernacexpr.rf_subclass = inst; rf_priority = pr; rf_notation = nots; rf_canonical = canon } ->
         if nots <> [] then Coq_elpi_utils.nYI "notation in record fields";
         if pr <> None then Coq_elpi_utils.nYI "priority in record fields";
-        if inst = Some false then Coq_elpi_utils.nYI "instance :>> flag in record fields";
         let atts = { Coq_elpi_HOAS.is_canonical = canon; is_coercion = inst <> None; name } in
         push_name gs fn.CAst.v, (intern_global_constr_ty gs x, atts) :: acc
     | Vernacexpr.DefExpr _, _ -> Coq_elpi_utils.nYI "DefExpr")

From 3a645158f21ae99b48dd0285cb45444a42a6fc7b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Tue, 6 Oct 2020 12:54:46 +0200
Subject: [PATCH 12/22] Adapt to coq/coq#13128 (instance_flag type change)

---
 src/coq_elpi_vernacular.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml
index 47470f672..cc5783fee 100644
--- a/src/coq_elpi_vernacular.ml
+++ b/src/coq_elpi_vernacular.ml
@@ -157,7 +157,7 @@ let intern_record_decl glob_sign { name; sort; parameters; constructor; fields }
     | Vernacexpr.AssumExpr ({ CAst.v = name } as fn,x), { Vernacexpr.rf_subclass = inst; rf_priority = pr; rf_notation = nots; rf_canonical = canon } ->
         if nots <> [] then Coq_elpi_utils.nYI "notation in record fields";
         if pr <> None then Coq_elpi_utils.nYI "priority in record fields";
-        let atts = { Coq_elpi_HOAS.is_canonical = canon; is_coercion = inst <> None; name } in
+        let atts = { Coq_elpi_HOAS.is_canonical = canon; is_coercion = inst <> Vernacexpr.NoInstance; name } in
         push_name gs fn.CAst.v, (intern_global_constr_ty gs x, atts) :: acc
     | Vernacexpr.DefExpr _, _ -> Coq_elpi_utils.nYI "DefExpr")
         (glob_sign_params,[]) fields in

From 577b56397c8b501f47738aa16a213635f5009d0e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 14 Oct 2020 19:43:16 +0200
Subject: [PATCH 13/22] Adapt to Coq #13166: AssumExpr takes a binder list.

For compatibility, we generalize the conclusion over the binders.
---
 src/coq_elpi_vernacular.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml
index cc5783fee..cf54c9330 100644
--- a/src/coq_elpi_vernacular.ml
+++ b/src/coq_elpi_vernacular.ml
@@ -154,10 +154,11 @@ let intern_record_decl glob_sign { name; sort; parameters; constructor; fields }
   let arity = intern_global_constr_ty glob_sign_params @@ CAst.make sort in
   let _, fields =
     List.fold_left (fun (gs,acc) -> function
-    | Vernacexpr.AssumExpr ({ CAst.v = name } as fn,x), { Vernacexpr.rf_subclass = inst; rf_priority = pr; rf_notation = nots; rf_canonical = canon } ->
+    | Vernacexpr.AssumExpr ({ CAst.v = name } as fn,bl,x), { Vernacexpr.rf_subclass = inst; rf_priority = pr; rf_notation = nots; rf_canonical = canon } ->
         if nots <> [] then Coq_elpi_utils.nYI "notation in record fields";
         if pr <> None then Coq_elpi_utils.nYI "priority in record fields";
         let atts = { Coq_elpi_HOAS.is_canonical = canon; is_coercion = inst <> Vernacexpr.NoInstance; name } in
+        let x = if bl = [] then x else Constrexpr_ops.mkCProdN bl x in
         push_name gs fn.CAst.v, (intern_global_constr_ty gs x, atts) :: acc
     | Vernacexpr.DefExpr _, _ -> Coq_elpi_utils.nYI "DefExpr")
         (glob_sign_params,[]) fields in

From f4c9ba6cd3f4b9d27a6610f4d896dbb84bd479de Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= <pierre-marie.pedrot@inria.fr>
Date: Wed, 23 Sep 2020 17:51:19 +0200
Subject: [PATCH 14/22] Fix w.r.t. coq/coq#13075.

---
 src/coq_elpi_HOAS.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml
index cb0781ff5..a596549a8 100644
--- a/src/coq_elpi_HOAS.ml
+++ b/src/coq_elpi_HOAS.ml
@@ -266,7 +266,7 @@ let abbreviation =
   }
 
 module GROrd = struct
-  include Names.GlobRef.Ordered
+  include Names.GlobRef.CanOrd
   let show x = Pp.string_of_ppcmds (Printer.pr_global x)
   let pp fmt x = Format.fprintf fmt "%s" (show x)
 end

From 25313d3fbbd9411f0d5d99bbf189eb2258f63c48 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Thu, 2 Jul 2020 17:16:00 +0200
Subject: [PATCH 15/22] [coq] Adapt to coq/coq#12611

---
 src/coq_elpi_builtins.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index 78b0911e1..8aa2132b8 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -1030,7 +1030,7 @@ Supported attributes:
      | Some field_specs -> (* record: projection... *)
          let names, flags =
            List.(split (map (fun { name; is_coercion; is_canonical } -> name,
-               { Record.pf_subclass = is_coercion ; pf_canonical = is_canonical })
+               { Record.Internal.pf_subclass = is_coercion ; pf_canonical = is_canonical })
              field_specs)) in
          let is_implicit = List.map (fun _ -> []) names in
          let cstr = (ind,1) in
@@ -1038,7 +1038,7 @@ Supported attributes:
          let k_ty = List.(hd (hd me.mind_entry_inds).mind_entry_lc) in
          let fields_as_relctx = Term.prod_assum k_ty in
          let kinds, sp_projs =
-           Record.declare_projections ind ~kind:Decls.Definition
+           Record.Internal.declare_projections ind ~kind:Decls.Definition
              (Evd.univ_entry ~poly:false sigma)
              (Names.Id.of_string "record")
              flags is_implicit fields_as_relctx
@@ -1051,7 +1051,7 @@ Supported attributes:
            s_EXPECTEDPARAM = npars;
          }
          in
-         Record.declare_structure_entry struc;
+         Record.Internal.declare_structure_entry struc;
      end;
      state, !: ind, []))),
   DocAbove);

From 034af87a82c09f4f2d914184c51f78bd808ba981 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Sat, 14 Nov 2020 01:10:21 +0100
Subject: [PATCH 16/22] [coq] Adapt to coq/coq#13312

---
 src/coq_elpi_builtins.ml | 4 ++--
 tests/test_HOAS.v        | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index 78b0911e1..0cf6a5380 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -517,8 +517,8 @@ let attribute_value = let open API.AlgebraicData in let open Attributes in let o
   pp = (fun fmt a -> Format.fprintf fmt "TODO");
   constructors = [
     K("leaf","",A(B.string,N),
-      B (fun s -> if s = "" then VernacFlagEmpty else VernacFlagLeaf s),
-      M (fun ~ok ~ko -> function VernacFlagEmpty -> ok "" | VernacFlagLeaf x -> ok x | _ -> ko ()));
+      B (fun s -> if s = "" then VernacFlagEmpty else VernacFlagLeaf (FlagString s)),
+      M (fun ~ok ~ko -> function VernacFlagEmpty -> ok "" | VernacFlagLeaf (FlagString x | FlagIdent x) -> ok x | _ -> ko ()));
     K("node","",C((fun self -> !> (B.list (attribute (!< self)))),N),
       B (fun l -> VernacFlagList l),
       M (fun ~ok ~ko -> function VernacFlagList l -> ok l | _ -> ko ())
diff --git a/tests/test_HOAS.v b/tests/test_HOAS.v
index 48029ee21..b34d07d2c 100644
--- a/tests/test_HOAS.v
+++ b/tests/test_HOAS.v
@@ -86,7 +86,7 @@ Elpi declarations
 Record foo A (B : A) : Type := {
     a of A & A : A;
     z (a : A) :>  B = B -> A;
-#[canonical(false)]
+#[canonical=no]
     x (w := 3) : forall x, a x x = x;
   }.
 
@@ -223,4 +223,4 @@ Elpi primitive (2000000003333002 + 1).
 
 From Coq Require Import Floats.
 Open Scope float_scope.
-Elpi primitive (2.4e13 + 1).
\ No newline at end of file
+Elpi primitive (2.4e13 + 1).

From 8c4ce1d3eeaff5ce6f3a1634d3c2236ab0d2f123 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Mon, 16 Nov 2020 11:13:30 +0100
Subject: [PATCH 17/22] Adapting to Coq PR #13386: new specific constructor
 Proj_cs for canonical structures.

I left the same TODO as in Const_cs.
---
 src/coq_elpi_builtins.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index dfd426571..30e249938 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -309,13 +309,19 @@ let cs_pattern =
   doc = "Pattern for canonical values";
   pp = (fun fmt -> function
     | Const_cs x -> Format.fprintf fmt "Const_cs %s" "<todo>"
+    | Proj_cs x -> Format.fprintf fmt "Proj_cs %s" "<todo>"
     | Prod_cs -> Format.fprintf fmt "Prod_cs"
     | Sort_cs _ ->  Format.fprintf fmt "Sort_cs"
     | Default_cs -> Format.fprintf fmt "Default_cs");
   constructors = [
     K("cs-gref","",A(gref,N),
-      B (fun x -> Const_cs x),
-      M (fun ~ok ~ko -> function Const_cs x -> ok x | _ -> ko ()));
+      B (function
+          | GlobRef.ConstructRef _ | GlobRef.IndRef _ | GlobRef.VarRef _ as x -> Const_cs x
+          | GlobRef.ConstRef cst as x ->
+          match Recordops.find_primitive_projection cst with
+          | None -> Const_cs x
+          | Some p -> Proj_cs p),
+      M (fun ~ok ~ko -> function Const_cs x -> ok x | Proj_cs p -> ok (GlobRef.ConstRef (Projection.Repr.constant p)) | _ -> ko ()));
     K("cs-prod","",N,
       B Prod_cs,
       M (fun ~ok ~ko -> function Prod_cs -> ok | _ -> ko ()));

From 6a0104d71d7742d81b26e6754f466c90a0b47925 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Wed, 25 Nov 2020 13:08:15 +0100
Subject: [PATCH 18/22] Adapt to coq/coq#13415 (interning/externing universes)

---
 src/coq_elpi_builtins.ml           | 7 +++++--
 src/coq_elpi_glob_quotation.ml     | 6 +++---
 src/coq_elpi_goal_HOAS.ml          | 6 +++---
 src/coq_elpi_vernacular.ml         | 4 ++--
 src/coq_elpi_vernacular.mli        | 2 +-
 src/coq_elpi_vernacular_syntax.mlg | 5 ++++-
 6 files changed, 18 insertions(+), 12 deletions(-)

diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index 30e249938..df4082f76 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -85,7 +85,7 @@ let add_universe_constraint state c =
   | Univ.UniverseInconsistency p ->
       Feedback.msg_debug
         (Univ.explain_universe_inconsistency
-           UnivNames.pr_with_global_universes p);
+           UnivNames.(pr_with_global_universes empty_binders) p);
       raise Pred.No_clause
   | Evd.UniversesDiffer | UState.UniversesDiffer ->
       Feedback.msg_debug Pp.(str"UniversesDiffer");
@@ -203,7 +203,10 @@ let closed_ground_term = {
 let term_skeleton =  {
   CConv.ty = Conv.TyName "term";
   pp_doc = (fun fmt () -> Format.fprintf fmt "A Coq term containing holes");
-  pp = (fun fmt t -> Format.fprintf fmt "%s" (Pp.string_of_ppcmds (Printer.pr_glob_constr_env (Global.env()) t)));
+  pp = (fun fmt t ->
+      let env = Global.env() in
+      let sigma = Evd.from_env env in
+      Format.fprintf fmt "%s" (Pp.string_of_ppcmds (Printer.pr_glob_constr_env env sigma t)));
   readback = lp2skeleton;
   embed = (fun ~depth _ _ _ _ -> assert false);
 }
diff --git a/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml
index 12cef2320..1359c504b 100644
--- a/src/coq_elpi_glob_quotation.ml
+++ b/src/coq_elpi_glob_quotation.ml
@@ -89,7 +89,7 @@ let type_gen = ref 0
 let rec gterm2lp ~depth state x =
   if debug () then
     Feedback.msg_debug Pp.(str"gterm2lp: depth=" ++ int depth ++
-      str " term=" ++Printer.pr_glob_constr_env (get_global_env state) x);
+      str " term=" ++Printer.pr_glob_constr_env (get_global_env state) (get_sigma state) x);
   match (DAst.get x) (*.CAst.v*) with
   | GRef(gr,_ul) -> state, in_elpi_gr ~depth state gr
   | GVar(id) ->
@@ -104,8 +104,8 @@ let rec gterm2lp ~depth state x =
       let state, s = API.RawQuery.mk_Arg state ~name:(Printf.sprintf "type_%d" !type_gen) ~args:[] in
       state, in_elpi_flex_sort s
   | GSort(UNamed [name,0]) ->
-      let env = get_global_env state in
-      state, in_elpi_sort (Sorts.sort_of_univ @@ Univ.Universe.make @@ Pretyping.interp_known_glob_level (Evd.from_env env) name)
+    let env = get_global_env state in
+      state, in_elpi_sort (Sorts.sort_of_univ @@ Univ.Universe.make @@ Pretyping.known_glob_level (Evd.from_env env) name)
   | GSort(_) -> nYI "(glob)HOAS for Type@{i j}"
 
   | GProd(name,_,s,t) ->
diff --git a/src/coq_elpi_goal_HOAS.ml b/src/coq_elpi_goal_HOAS.ml
index 1fda4a176..fcaec6418 100644
--- a/src/coq_elpi_goal_HOAS.ml
+++ b/src/coq_elpi_goal_HOAS.ml
@@ -68,7 +68,7 @@ let rec list_map_acc f acc = function
       let acc, xs = list_map_acc f acc xs in
       acc, x :: xs
 
-let contract_params env name params t =
+let contract_params env sigma name params t =
   let open Glob_term in
   let loc = Option.map Coq_elpi_utils.of_coq_loc t.CAst.loc in
   let rec contract params args =
@@ -85,7 +85,7 @@ let contract_params env name params t =
        | GHole _ -> contract ps rest
        | _ -> Coq_elpi_utils.err ?loc Pp.(str "Inductive type "++ Names.Id.print name ++
                 str" is not applied to parameter " ++ Names.Id.print pname ++
-                str" but rather " ++ Printer.pr_glob_constr_env env arg)
+                str" but rather " ++ Printer.pr_glob_constr_env env sigma arg)
        end
     in
   let rec aux x =
@@ -102,7 +102,7 @@ let contract_params env name params t =
 let ginductive2lp ~depth state { finiteness; name; arity; params; nuparams; constructors } =
   let open Coq_elpi_glob_quotation in
   let space, indt_name = name in
-  let contract state x = contract_params (get_global_env state) indt_name params x in
+  let contract state x = contract_params (get_global_env state) (get_sigma state) indt_name params x in
   let do_constructor ~depth state (name, ty) =
     let state, ty = do_params nuparams (do_arity (contract state ty)) ~depth state in
     state, in_elpi_indtdecl_constructor (Name.Name name) ty
diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml
index cf54c9330..e64cdf2d7 100644
--- a/src/coq_elpi_vernacular.ml
+++ b/src/coq_elpi_vernacular.ml
@@ -56,7 +56,7 @@ let _pp_qualified_name fmt l = Format.fprintf fmt "%s" (String.concat "." l)
 type expr_record_decl = {
   name : qualified_name;
   parameters : Constrexpr.local_binder_expr list;
-  sort : Glob_term.glob_sort option;
+  sort : Constrexpr.sort_expr option;
   constructor : Names.Id.t option;
   fields : (Vernacexpr.local_decl_expr * Vernacexpr.record_field_attr) list
 }
@@ -137,7 +137,7 @@ let intern_global_constr_ty { Ltac_plugin.Tacintern.genv = env } ?(intern_env=Co
   Constrintern.intern_gen Pretyping.IsType env sigma ~impls:intern_env ~pattern_mode:false ~ltacvars:Constrintern.empty_ltac_sign t
 
 let intern_global_context { Ltac_plugin.Tacintern.genv = env } ?(intern_env=Constrintern.empty_internalization_env) ctx =
-  Constrintern.intern_context env intern_env ctx
+  Constrintern.intern_context env ~bound_univs:UnivNames.empty_binders intern_env ctx
 
 let subst_global_constr s t = Detyping.subst_glob_constr (Global.env()) s t
 let subst_global_decl s (n,bk,ot,t) =
diff --git a/src/coq_elpi_vernacular.mli b/src/coq_elpi_vernacular.mli
index f093b8b87..cb63d1a0c 100644
--- a/src/coq_elpi_vernacular.mli
+++ b/src/coq_elpi_vernacular.mli
@@ -37,7 +37,7 @@ val print : qualified_name -> string list -> unit
 type expr_record_decl = {
   name : qualified_name;
   parameters : Constrexpr.local_binder_expr list;
-  sort : Glob_term.glob_sort option;
+  sort : Constrexpr.sort_expr option;
   constructor : Names.Id.t option;
   fields : (Vernacexpr.local_decl_expr * Vernacexpr.record_field_attr) list
 }
diff --git a/src/coq_elpi_vernacular_syntax.mlg b/src/coq_elpi_vernacular_syntax.mlg
index 66dfe1e35..e3f53ba3e 100644
--- a/src/coq_elpi_vernacular_syntax.mlg
+++ b/src/coq_elpi_vernacular_syntax.mlg
@@ -158,7 +158,10 @@ let pr_glob_constr_and_expr = function
     let env = Global.env () in
     let sigma = Evd.from_env env in
     Ppconstr.pr_constr_expr env sigma c
-  | (c, None) -> Printer.pr_glob_constr_env (Global.env ()) c
+  | (c, None) ->
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    Printer.pr_glob_constr_env env sigma c
 
 let pp_elpi_arg _ _ _ = EV.pr_arg (fun (_,x) -> pr_glob_constr_and_expr x) (fun (_,r) -> Coq_elpi_goal_HOAS.pr_glob_record_decl r) (fun (_,r) -> Coq_elpi_goal_HOAS.pr_glob_indt_decl r) (fun (_,r) -> Coq_elpi_goal_HOAS.pr_glob_constant_decl r) (fun (_,x) -> Coq_elpi_goal_HOAS.pr_glob_context_decl x)
 let pp_glob_elpi_arg _ _ _ = EV.pr_arg pr_glob_constr_and_expr Coq_elpi_goal_HOAS.pr_glob_record_decl Coq_elpi_goal_HOAS.pr_glob_indt_decl Coq_elpi_goal_HOAS.pr_glob_constant_decl  Coq_elpi_goal_HOAS.pr_glob_context_decl

From c2d76f10749eb4d2dd074015162dd4576897966e Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Thu, 10 Dec 2020 11:23:48 +0100
Subject: [PATCH 19/22] move master on Coq 8.13

---
 .github/workflows/main.yml | 28 +++++-----------------------
 coq-elpi.opam              |  2 +-
 2 files changed, 6 insertions(+), 24 deletions(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index bc32d434a..e7271271e 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -16,7 +16,7 @@ jobs:
     strategy:
       matrix:
         coq_version:
-          - dev
+          - '8.13'
         ocaml_version:
           - 'minimal'
     steps:
@@ -26,26 +26,8 @@ jobs:
         opam_file: './coq-elpi.opam'
         coq_version: ${{ matrix.coq_version }}
         ocaml_version: ${{ matrix.ocaml_version }}
-        custom_script: |
-          startGroup Print opam config
-            opam config list; opam repo list; opam list
-          endGroup
-          startGroup Build dependencies
-            opam pin add -n -y -k path $PACKAGE $WORKDIR
-            opam update -y
-            opam install -y -j 4 $PACKAGE --deps-only
-          endGroup
-          startGroup List installed packages
-            opam list
-          endGroup
-          startGroup Build
-            opam install -y -v -j 4 $PACKAGE
-            opam list
-          endGroup
-          startGroup Test Hierarchy Builder
+        after_script: |
+          startGroup "Test HB"
             opam pin add coq-hierarchy-builder 'https://github.com/math-comp/hierarchy-builder.git' --ignore-constraints-on=coq-elpi -y -j 4
-            opam remove coq-hierarchy-builder -y
-          endGroup
-          startGroup Uninstallation test
-            opam remove $PACKAGE -y
-          endGroup
+            opam list
+          endGroup
\ No newline at end of file
diff --git a/coq-elpi.opam b/coq-elpi.opam
index 3287c68e8..d3c800655 100644
--- a/coq-elpi.opam
+++ b/coq-elpi.opam
@@ -12,7 +12,7 @@ build: [ make "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" ]
 install: [ make "install" "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" ]
 depends: [
   "elpi" {>= "1.12.0" & < "1.13.0~"}
-  "coq" {= "dev"}
+  "coq" {>= "8.13" & < "8.14~" }
   ]
 tags: [ "logpath:elpi" ]
 synopsis: "Elpi extension language for Coq"

From f4872f5733aada9521f26e7724dcd609599a27ac Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Thu, 10 Dec 2020 15:11:12 +0100
Subject: [PATCH 20/22] update changelog

---
 .github/workflows/main.yml | 2 +-
 Changelog.md               | 4 ++++
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index e7271271e..65717b644 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -28,6 +28,6 @@ jobs:
         ocaml_version: ${{ matrix.ocaml_version }}
         after_script: |
           startGroup "Test HB"
-            opam pin add coq-hierarchy-builder 'https://github.com/math-comp/hierarchy-builder.git' --ignore-constraints-on=coq-elpi -y -j 4
+            opam pin add coq-hierarchy-builder https://github.com/math-comp/hierarchy-builder.git --ignore-constraints-on=coq-elpi -y -j 4
             opam list
           endGroup
\ No newline at end of file
diff --git a/Changelog.md b/Changelog.md
index 984a89b0d..616819e47 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,5 +1,9 @@
 # Changelog
 
+## [1.8.1] - 10-12-2020
+
+Requires Elpi 1.12 and Coq 8.13.
+
 ## [1.8.0] - 29-11-2020
 
 Requires Elpi 1.12 and Coq 8.12.

From 1af9ca5a1d9ba97f47e2bd7c0329f2d2297bdfd8 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Thu, 10 Dec 2020 15:58:29 +0100
Subject: [PATCH 21/22] fix script

---
 .github/workflows/main.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 65717b644..d33740b6f 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -30,4 +30,5 @@ jobs:
           startGroup "Test HB"
             opam pin add coq-hierarchy-builder https://github.com/math-comp/hierarchy-builder.git --ignore-constraints-on=coq-elpi -y -j 4
             opam list
+            opam remove coq-hierarchy-builder -y
           endGroup
\ No newline at end of file

From cb382e4a41de09b406d3ab15eb5dc302d9a84bd1 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Fri, 11 Dec 2020 10:59:04 +0100
Subject: [PATCH 22/22] [HOAS] deal with illformed grefs (fix #189)

---
 Changelog.md             |  7 ++++++-
 src/coq_elpi_HOAS.ml     | 20 +++++++++++++++-----
 src/coq_elpi_HOAS.mli    |  1 +
 src/coq_elpi_builtins.ml | 10 +++++++++-
 tests/test_API.v         | 20 ++++++++++++++++++++
 theories/elpi.v          |  8 ++++++++
 6 files changed, 59 insertions(+), 7 deletions(-)

diff --git a/Changelog.md b/Changelog.md
index 616819e47..c09a4979f 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,8 +1,13 @@
 # Changelog
 
-## [1.8.1] - 10-12-2020
+## [1.8.1] - 11-12-2020
 
 Requires Elpi 1.12 and Coq 8.13.
+### HOAS
+- Illformed terms like `global (const X)` (which have no
+  representation in Coq) are now reported with a proper error message.
+  Whe passed to `coq.term->string`, instead of a fatal error, we pick for
+  the illformed sub term the `unknown_gref` special constant.
 
 ## [1.8.0] - 29-11-2020
 
diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml
index 9e6171cf4..853c8cfa0 100644
--- a/src/coq_elpi_HOAS.ml
+++ b/src/coq_elpi_HOAS.ml
@@ -78,6 +78,7 @@ type options = {
   local : bool option;
   deprecation : Deprecation.t option;
   primitive : bool option;
+  failsafe : bool; (* don't fail, e.g. we are trying to print a term *)
 }
 
 let default_options = {
@@ -85,6 +86,7 @@ let default_options = {
   local = None;
   deprecation = None;
   primitive = None;
+  failsafe = false;
 }
 
 type 'a coq_context = {
@@ -282,10 +284,17 @@ let in_elpi_gr ~depth s r =
   assert (gl = []);
   E.mkApp globalc t []
 
-let in_coq_gref ~depth s t =
-  let s, t, gls = gref.API.Conversion.readback ~depth s t in
-  assert(gls = []);
-  s, t
+let in_coq_gref ~depth ~origin ~failsafe s t =
+  try
+    let s, t, gls = gref.API.Conversion.readback ~depth s t in
+    assert(gls = []);
+    s, t
+  with API.Conversion.TypeErr _ ->
+    if failsafe then
+      s, Coqlib.lib_ref "elpi.unknown_gref"
+    else
+      err Pp.(str "The term " ++ str(pp2string (P.term depth) origin) ++
+        str " cannot be represented in Coq since its gref part is illformed")
 
 let mpin, ismp, mpout, modpath =
   let { CD.cin; isc; cout }, x = CD.declare {
@@ -617,6 +626,7 @@ let get_options ~depth hyps state =
     local = locality @@ get_string_option "coq:locality";
     deprecation = deprecation @@ get_pair_option API.BuiltInData.string API.BuiltInData.string "coq:deprecation";
     primitive = get_bool_option "coq:primitive";
+    failsafe = false;
   }
 
 let mk_coq_context ~options state =
@@ -1097,7 +1107,7 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals
       state, EC.mkSort u, gsl
  (* constants *)
   | E.App(c,d,[]) when globalc == c ->
-     let state, gr = in_coq_gref ~depth state d in
+     let state, gr = in_coq_gref ~depth ~origin:t ~failsafe:coq_ctx.options.failsafe state d in
      begin match gr with
      | G.VarRef x -> state, EC.mkVar x, []
      | G.ConstRef x -> state, EC.mkConst x, []
diff --git a/src/coq_elpi_HOAS.mli b/src/coq_elpi_HOAS.mli
index bf96fdb10..ac303cb0e 100644
--- a/src/coq_elpi_HOAS.mli
+++ b/src/coq_elpi_HOAS.mli
@@ -20,6 +20,7 @@ type options = {
   local : bool option;
   deprecation : Deprecation.t option;
   primitive : bool option;
+  failsafe : bool; (* readback is resilient to illformed terms *)
 }
 
 type 'a coq_context = {
diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index 6e1904e1a..e859cece5 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -176,6 +176,14 @@ let term = {
   readback = lp2constr;
   embed = constr2lp;
 }
+let failsafe_term = {
+  CConv.ty = Conv.TyName "term";
+  pp_doc = (fun fmt () -> Format.fprintf fmt "A Coq term containing evars");
+  pp = (fun fmt t -> Format.fprintf fmt "%s" (Pp.string_of_ppcmds (Printer.pr_econstr_env (Global.env()) Evd.empty t)));
+  readback = (fun ~depth coq_ctx csts s t -> lp2constr ~depth { coq_ctx with options = { coq_ctx.options with failsafe = true }} csts s t);
+  embed = constr2lp;
+}
+
 let proof_context : (full coq_context, API.Data.constraints) CConv.ctx_readback =
   fun ~depth hyps constraints state ->
     let state, proof_context, _, gls = get_current_env_sigma ~depth hyps constraints state in
@@ -2024,7 +2032,7 @@ coq.id->name S N :- coq.string->name S N.
   DocAbove);
 
   MLCode(Pred("coq.term->string",
-    CIn(term,"T",
+    CIn(failsafe_term,"T",
     Out(B.string, "S",
     Full(proof_context, "prints a term T to a string S using Coq's pretty printer"))),
   (fun t _ ~depth proof_context constraints state ->
diff --git a/tests/test_API.v b/tests/test_API.v
index a32896441..1ba170461 100644
--- a/tests/test_API.v
+++ b/tests/test_API.v
@@ -140,6 +140,26 @@ Elpi Query lp:{{
 
 }}.
 
+Elpi Tactic test.
+Elpi Accumulate lp:{{
+solve _ _ _ :-
+  coq.term->string X S,
+  X = global (indc Y),
+  coq.say S.
+}}.
+Goal True.
+Fail elpi test.
+Abort.
+
+Elpi Tactic test2.
+Elpi Accumulate lp:{{
+solve _ _ _ :-
+  coq.term->string (global (indc Y)) S,
+  coq.say S.
+}}.
+Goal True.
+elpi test2.
+Abort.
 
 End elab.
 (****** say *************************************)
diff --git a/theories/elpi.v b/theories/elpi.v
index 5c650130f..aa5178d69 100644
--- a/theories/elpi.v
+++ b/theories/elpi.v
@@ -19,6 +19,14 @@ Register hole as elpi.hole.
 Inductive unknown_inductive : Prop := unknown_constructor.
 Register unknown_inductive as elpi.unknown_inductive.
 
+(* Special global constant used to signal a datum of type gref which
+   has no corresponding Coq global reference. This typically signals
+   an error: a term like (global (const X)) has no meaning in Coq, X must
+   be an actual name.
+*)
+Inductive unknown_gref : Prop := .
+Register unknown_gref as elpi.unknown_gref.
+
 (* Common constants available inside Coq's syntax {{ ... lib:<name> ... }} *)
 Register Coq.Init.Logic.eq      as elpi.eq.
 Register Coq.Init.Logic.eq_refl as elpi.erefl.