From 19f5f05dc868334ec94371ad910af6b5904ca250 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Sat, 29 Feb 2020 22:34:46 +0100
Subject: [PATCH 1/3] minimized test case for universes inside section

---
 theories/tests/test_HOAS.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/theories/tests/test_HOAS.v b/theories/tests/test_HOAS.v
index bc744ddd3..9997c2789 100644
--- a/theories/tests/test_HOAS.v
+++ b/theories/tests/test_HOAS.v
@@ -87,3 +87,11 @@ Elpi Accumulate lp:{{
 Elpi Typecheck.
 
 Elpi kwd fun in as 4 end match return => : := { } ; , | "x" 1 H (match x as y in False return nat with end).
+
+Elpi Query lp:{{
+  coq.env.begin-section "xxxxx",
+  coq.univ.new [] U,
+  T = sort (typ U),
+  coq.env.add-const "a" _ T tt tt _,
+  coq.env.end-section
+}}.
\ No newline at end of file

From 4f4517431d22875b0095c5ac2700618eb73a365c Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Sun, 1 Mar 2020 11:17:24 +0100
Subject: [PATCH 2/3] fix universes of section variables

---
 src/coq_elpi_builtins.ml | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index 7f17fde9f..b6e0e27e0 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -861,16 +861,24 @@ It undestands qualified names, e.g. "Nat.t".|})),
        | Given ty ->
        let used = EConstr.universes_of_constr sigma ty in
        let sigma = Evd.restrict_universe_context sigma used in
+       let ubinders = Evd.universe_binders sigma in
+       let uentry = Evd.univ_entry ~poly:false sigma in
        let kind = Decls.Logical in
        let impargs = [] in
        let variable = CAst.(make @@ Id.of_string id) in
        let gr, _ =
          if local then begin
+           let uctx =
+              let context_set_of_entry = function
+                | Entries.Polymorphic_entry (_,uctx) -> Univ.ContextSet.of_context uctx
+                | Entries.Monomorphic_entry uctx -> uctx in
+              context_set_of_entry uentry in
+           Declare.declare_universe_context ~poly:false uctx;
            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)
-             (Evd.univ_entry ~poly:false sigma, UnivNames.empty_binders) impargs Declaremods.NoInline
+             (uentry, ubinders) impargs Declaremods.NoInline
              variable
        in
        state, !: (global_constant_of_globref gr), []

From 1856a5a3098e9a62e569c70086d36740871855fe Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Sun, 1 Mar 2020 11:23:26 +0100
Subject: [PATCH 3/3] travis: do not run PRs twice

---
 .travis.yml | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/.travis.yml b/.travis.yml
index 81fc79f98..18528fbd3 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -5,6 +5,11 @@ language: c
 git:
   submodules: false
 
+banches:
+  only:
+  - master
+  - coq-master
+
 install:
  - curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh > install.sh
  - echo | sudo sh install.sh