From dfcc22eeb6e5404a42d28917a5540e1d894b5a71 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 23 Mar 2020 03:43:26 -0400
Subject: [ci] [overlays] Adapt to declare API changes.

- problem with metacoq overlay ; it expects to send a non-ground
  constant to the kernel, now it fails at prepare.

Record Sigma (A : Type) (B : A -> Type) : Type :=
  { fst : A ; snd : B fst }.
Arguments fst {A B}.
Arguments snd {A B}.

Quote Recursively Definition foo := (fst, snd).

There is a hack on the overlay, we need to discuss it a bit more.
---
 ...oof+remove_special_case_first_declaration_in_mutual.sh | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh

(limited to 'dev')

diff --git a/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh b/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh
new file mode 100644
index 0000000000..e3a8eb07f3
--- /dev/null
+++ b/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh
@@ -0,0 +1,15 @@
+if [ "$CI_PULL_REQUEST" = "11818" ] || [ "$CI_BRANCH" = "proof+remove_special_case_first_declaration_in_mutual" ]; then
+
+    metacoq_CI_REF=proof+remove_special_case_first_declaration_in_mutual
+    metacoq_CI_GITURL=https://github.com/ejgallego/metacoq
+
+    elpi_CI_REF=proof+remove_special_case_first_declaration_in_mutual
+    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+    paramcoq_CI_REF=proof+remove_special_case_first_declaration_in_mutual
+    paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
+
+    equations_CI_REF=proof+remove_special_case_first_declaration_in_mutual
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi
-- 
cgit v1.2.3