diff options
Diffstat (limited to 'dev')
38 files changed, 0 insertions, 403 deletions
diff --git a/dev/ci/user-overlays/08726-herbelin-master+more-stable-meaning-to-Discharge-flag.sh b/dev/ci/user-overlays/08726-herbelin-master+more-stable-meaning-to-Discharge-flag.sh deleted file mode 100644 index 242b177d71..0000000000 --- a/dev/ci/user-overlays/08726-herbelin-master+more-stable-meaning-to-Discharge-flag.sh +++ /dev/null @@ -1,23 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8726" ] || [ "$CI_BRANCH" = "master+more-stable-meaning-to-Discharge-flag" ]; then - - fiat_parsers_CI_BRANCH=master+change-for-coq-pr8726 - fiat_parsers_CI_REF=master+change-for-coq-pr8726 - fiat_parsers_CI_GITURL=https://github.com/herbelin/fiat - - elpi_CI_BRANCH=coq-master+fix-global-pr8726 - elpi_CI_REF=coq-master+fix-global-pr8726 - elpi_CI_GITURL=https://github.com/herbelin/coq-elpi - - equations_CI_BRANCH=master+fix-global-pr8726 - equations_CI_REF=master+fix-global-pr8726 - equations_CI_GITURL=https://github.com/herbelin/Coq-Equations - - mtac2_CI_BRANCH=master+fix-global-pr8726 - mtac2_CI_REF=master+fix-global-pr8726 - mtac2_CI_GITURL=https://github.com/herbelin/Mtac2 - - paramcoq_CI_BRANCH=master+fix-global-pr8726 - paramcoq_CI_REF=master+fix-global-pr8726 - paramcoq_CI_GITURL=https://github.com/herbelin/paramcoq - -fi diff --git a/dev/ci/user-overlays/09566-ejgallego-proof_global+move_termination_routine_out.sh b/dev/ci/user-overlays/09566-ejgallego-proof_global+move_termination_routine_out.sh deleted file mode 100644 index e4cf74aa51..0000000000 --- a/dev/ci/user-overlays/09566-ejgallego-proof_global+move_termination_routine_out.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9566" ] || [ "$CI_BRANCH" = "proof_global+move_termination_routine_out" ]; then - - aac_tactics_CI_REF=proof_global+move_termination_routine_out - aac_tactics_CI_GITURL=https://github.com/ejgallego/aac-tactics - - equations_CI_REF=proof_global+move_termination_routine_out - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - paramcoq_CI_REF=proof_global+move_termination_routine_out - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - -fi diff --git a/dev/ci/user-overlays/09645-ejgallego-proof+sayonara_baby.sh b/dev/ci/user-overlays/09645-ejgallego-proof+sayonara_baby.sh deleted file mode 100644 index 3029f3019c..0000000000 --- a/dev/ci/user-overlays/09645-ejgallego-proof+sayonara_baby.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9645" ] || [ "$CI_BRANCH" = "proof+sayonara_baby" ]; then - - equations_CI_REF=proof+sayonara_baby - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - mtac2_CI_REF=proof+sayonara_baby - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - - paramcoq_CI_REF=proof+sayonara_baby - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - -fi diff --git a/dev/ci/user-overlays/09867-primitive-floats.sh b/dev/ci/user-overlays/09867-primitive-floats.sh deleted file mode 100644 index a0e9085afd..0000000000 --- a/dev/ci/user-overlays/09867-primitive-floats.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9867" ] || [ "$CI_BRANCH" = "primitive-floats" ]; then - - unicoq_CI_REF=primitive-floats - unicoq_CI_GITURL=https://github.com/validsdp/unicoq - - elpi_CI_REF=primitive-floats - elpi_CI_GITURL=https://github.com/validsdp/coq-elpi - - coqhammer_CI_REF=primitive-floats - coqhammer_CI_GITURL=https://github.com/validsdp/coqhammer - -fi diff --git a/dev/ci/user-overlays/10204-rm-unsafe-type-of-coercion.sh b/dev/ci/user-overlays/10204-rm-unsafe-type-of-coercion.sh deleted file mode 100644 index 87dad61dbc..0000000000 --- a/dev/ci/user-overlays/10204-rm-unsafe-type-of-coercion.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10204" ] || [ "$CI_BRANCH" = "rm-unsafe-type-of-coercion" ]; then - - paramcoq_CI_REF=fix-papp - paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq - -fi diff --git a/dev/ci/user-overlays/10231-herbelin-master+locating-warning-different-implicit-term-type.sh b/dev/ci/user-overlays/10231-herbelin-master+locating-warning-different-implicit-term-type.sh deleted file mode 100644 index c8cf85e73e..0000000000 --- a/dev/ci/user-overlays/10231-herbelin-master+locating-warning-different-implicit-term-type.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10231" ] || [ "$CI_BRANCH" = "master+locating-warning-different-implicit-term-type" ]; then - - equations_CI_REF=master+fix-manual-implicit-pr10231 - equations_CI_GITURL=https://github.com/herbelin/Coq-Equations - - mtac2_CI_REF=master+fix-manual-implicit-pr10231 - mtac2_CI_GITURL=https://github.com/herbelin/Mtac2 - -fi diff --git a/dev/ci/user-overlays/10316-ejgallego-proof+recthms.sh b/dev/ci/user-overlays/10316-ejgallego-proof+recthms.sh deleted file mode 100644 index d133bc9993..0000000000 --- a/dev/ci/user-overlays/10316-ejgallego-proof+recthms.sh +++ /dev/null @@ -1,18 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10316" ] || [ "$CI_BRANCH" = "proof+recthms" ]; then - - elpi_CI_REF=proof+recthms - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - - equations_CI_REF=proof+recthms - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - mtac2_CI_REF=proof+recthms - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - - paramcoq_CI_REF=proof+recthms - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - - quickchick_CI_REF=proof+recthms - quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick - -fi diff --git a/dev/ci/user-overlays/10319-SkySkimmer-vernac-when-sideff.sh b/dev/ci/user-overlays/10319-SkySkimmer-vernac-when-sideff.sh deleted file mode 100644 index c5f1510357..0000000000 --- a/dev/ci/user-overlays/10319-SkySkimmer-vernac-when-sideff.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10319" ] || [ "$CI_BRANCH" = "vernac-when-sideff" ]; then - - mtac2_CI_REF=vernac-when-sideff - mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2 - - equations_CI_REF=vernac-when-sideff - equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/10334-ppedrot-rm-kernel-sideeff-role.sh b/dev/ci/user-overlays/10334-ppedrot-rm-kernel-sideeff-role.sh deleted file mode 100644 index 2c3f490c03..0000000000 --- a/dev/ci/user-overlays/10334-ppedrot-rm-kernel-sideeff-role.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10334" ] || [ "$CI_BRANCH" = "rm-kernel-sideeff-role" ]; then - - equations_CI_REF=rm-kernel-sideeff-role - equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/10337-ejgallego-vernac+qed_special_case_inject_proof.sh b/dev/ci/user-overlays/10337-ejgallego-vernac+qed_special_case_inject_proof.sh deleted file mode 100644 index 288e14c866..0000000000 --- a/dev/ci/user-overlays/10337-ejgallego-vernac+qed_special_case_inject_proof.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10337" ] || [ "$CI_BRANCH" = "vernac+qed_special_case_inject_proof" ]; then - - paramcoq_CI_REF=vernac+qed_special_case_inject_proof - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - - equations_CI_REF=vernac+qed_special_case_inject_proof - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/10362-ppedrot-delay-poly-opaque.sh b/dev/ci/user-overlays/10362-ppedrot-delay-poly-opaque.sh deleted file mode 100644 index 735b2ebbc3..0000000000 --- a/dev/ci/user-overlays/10362-ppedrot-delay-poly-opaque.sh +++ /dev/null @@ -1,15 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10362" ] || [ "$CI_BRANCH" = "delay-poly-opaque" ]; then - - paramcoq_CI_REF=delay-poly-opaque - paramcoq_CI_GITURL=https://github.com/ppedrot/paramcoq - - elpi_CI_REF=delay-poly-opaque - elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi - - coqhammer_CI_REF=delay-poly-opaque - coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer - - coq_dpdgraph_CI_REF=delay-poly-opaque - coq_dpdgraph_CI_GITURL=https://github.com/ppedrot/coq-dpdgraph - -fi diff --git a/dev/ci/user-overlays/10406-ppedrot-desync-entry-proof.sh b/dev/ci/user-overlays/10406-ppedrot-desync-entry-proof.sh deleted file mode 100644 index 3122f953de..0000000000 --- a/dev/ci/user-overlays/10406-ppedrot-desync-entry-proof.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10406" ] || [ "$CI_BRANCH" = "desync-entry-proof" ]; then - - equations_CI_REF=desync-entry-proof - equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - - quickchick_CI_REF=desync-entry-proof - quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick - -fi diff --git a/dev/ci/user-overlays/10419-ejgallego-heads+test.sh b/dev/ci/user-overlays/10419-ejgallego-heads+test.sh deleted file mode 100644 index 0ec0c3673a..0000000000 --- a/dev/ci/user-overlays/10419-ejgallego-heads+test.sh +++ /dev/null @@ -1,18 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10419" ] || [ "$CI_BRANCH" = "heads+test" ]; then - - elpi_CI_REF=heads+test - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - - equations_CI_REF=heads+test - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - mtac2_CI_REF=heads+test - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - - paramcoq_CI_REF=heads+test - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - - quickchick_CI_REF=heads+test - quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick - -fi diff --git a/dev/ci/user-overlays/10434-ejgallego-proof+hook_record.sh b/dev/ci/user-overlays/10434-ejgallego-proof+hook_record.sh deleted file mode 100644 index 3a2f4e1001..0000000000 --- a/dev/ci/user-overlays/10434-ejgallego-proof+hook_record.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10434" ] || [ "$CI_BRANCH" = "proof+hook_record" ]; then - - equations_CI_REF=proof+hook_record - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - mtac2_CI_REF=proof+hook_record - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - - paramcoq_CI_REF=proof+hook_record - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - -fi diff --git a/dev/ci/user-overlays/10441-ppedrot-static-poly-section.sh b/dev/ci/user-overlays/10441-ppedrot-static-poly-section.sh deleted file mode 100644 index 00f544f894..0000000000 --- a/dev/ci/user-overlays/10441-ppedrot-static-poly-section.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10441" ] || [ "$CI_BRANCH" = "static-poly-section" ]; then - - ext_lib_CI_REF=static-poly-section - ext_lib_CI_GITURL=https://github.com/ppedrot/coq-ext-lib - -fi diff --git a/dev/ci/user-overlays/10476-maximedenes-rm-library-optim.sh b/dev/ci/user-overlays/10476-maximedenes-rm-library-optim.sh deleted file mode 100644 index 10526a9ffe..0000000000 --- a/dev/ci/user-overlays/10476-maximedenes-rm-library-optim.sh +++ /dev/null @@ -1,10 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10476" ] || [ "$CI_BRANCH" = "rm-library-optim" ]; then - - sf_lf_CI_TARURL=https://www.maximedenes.fr/download/lf.tgz - sf_plf_CI_TARURL=https://www.maximedenes.fr/download/plf.tgz - sf_vfa_CI_TARURL=https://www.maximedenes.fr/download/vfa.tgz - - vst_CI_REF=fix-export - vst_CI_GITURL=https://github.com/maximedenes/VST - -fi diff --git a/dev/ci/user-overlays/10516-ejgallego-proof+dup_save.sh b/dev/ci/user-overlays/10516-ejgallego-proof+dup_save.sh deleted file mode 100644 index 7001c3d0c8..0000000000 --- a/dev/ci/user-overlays/10516-ejgallego-proof+dup_save.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10516" ] || [ "$CI_BRANCH" = "proof+dup_save" ]; then - - elpi_CI_REF=proof+dup_save - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - -fi diff --git a/dev/ci/user-overlays/10642-SkySkimmer-feedback-added-axiom.sh b/dev/ci/user-overlays/10642-SkySkimmer-feedback-added-axiom.sh deleted file mode 100644 index 413805e8e9..0000000000 --- a/dev/ci/user-overlays/10642-SkySkimmer-feedback-added-axiom.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10642" ] || [ "$CI_BRANCH" = "feedback-added-axiom" ]; then - - elpi_CI_REF=feedback-added-axiom - elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi - -fi diff --git a/dev/ci/user-overlays/10660-ejgallego-errors+private.sh b/dev/ci/user-overlays/10660-ejgallego-errors+private.sh deleted file mode 100644 index 21ff60493b..0000000000 --- a/dev/ci/user-overlays/10660-ejgallego-errors+private.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10660" ] || [ "$CI_BRANCH" = "errors+private" ]; then - - coqhammer_CI_REF=errors+private - coqhammer_CI_GITURL=https://github.com/ejgallego/coqhammer - -fi diff --git a/dev/ci/user-overlays/10665-ejgallego-api+varkind.sh b/dev/ci/user-overlays/10665-ejgallego-api+varkind.sh deleted file mode 100644 index 0c47f6a60b..0000000000 --- a/dev/ci/user-overlays/10665-ejgallego-api+varkind.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10665" ] || [ "$CI_BRANCH" = "api+varkind" ]; then - - elpi_CI_REF=api+varkind - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - - quickchick_CI_REF=api+varkind - quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick - -fi diff --git a/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh b/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh deleted file mode 100644 index 6dc44aa627..0000000000 --- a/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10674" ] || [ "$CI_BRANCH" = "proofs+declare_unif" ]; then - - equations_CI_REF=proofs+declare_unif - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/10681-ejgallego-proof+private_entry.sh b/dev/ci/user-overlays/10681-ejgallego-proof+private_entry.sh deleted file mode 100644 index f4840c2a83..0000000000 --- a/dev/ci/user-overlays/10681-ejgallego-proof+private_entry.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10681" ] || [ "$CI_BRANCH" = "proof+private_entry" ]; then - - equations_CI_REF=proof+private_entry - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh b/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh deleted file mode 100644 index a5f6551474..0000000000 --- a/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10727" ] || [ "$CI_BRANCH" = "library+to_vernac_step2" ]; then - - elpi_CI_REF=library+to_vernac_step2 - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - -fi diff --git a/dev/ci/user-overlays/10811-SkySkimmer-sprop-default-on.sh b/dev/ci/user-overlays/10811-SkySkimmer-sprop-default-on.sh deleted file mode 100644 index d7af6b7a36..0000000000 --- a/dev/ci/user-overlays/10811-SkySkimmer-sprop-default-on.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10811" ] || [ "$CI_BRANCH" = "sprop-default-on" ]; then - - elpi_CI_REF=sprop-default-on - elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi - - coq_dpdgraph_CI_REF=sprop-default-on - coq_dpdgraph_CI_GITURL=https://github.com/SkySkimmer/coq-dpdgraph - -fi diff --git a/dev/ci/user-overlays/10832-herbelin-master+fix6082-7766-overriding-notation-format.sh b/dev/ci/user-overlays/10832-herbelin-master+fix6082-7766-overriding-notation-format.sh deleted file mode 100644 index c17fe4fcba..0000000000 --- a/dev/ci/user-overlays/10832-herbelin-master+fix6082-7766-overriding-notation-format.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10832" ] || [ "$CI_BRANCH" = "master+fix6082-7766-overriding-notation-format" ]; then - - equations_CI_REF=master+fix-interpretation-notation-format-pr10832 - equations_CI_GITURL=https://github.com/herbelin/Coq-Equations - - quickchick_CI_REF=master+fix-interpretation-notation-format-pr10832 - quickchick_CI_GITURL=https://github.com/herbelin/QuickChick - -fi diff --git a/dev/ci/user-overlays/11027-SkySkimmer-expose-comind-univ.sh b/dev/ci/user-overlays/11027-SkySkimmer-expose-comind-univ.sh deleted file mode 100644 index bb65beb043..0000000000 --- a/dev/ci/user-overlays/11027-SkySkimmer-expose-comind-univ.sh +++ /dev/null @@ -1,19 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11027" ] || [ "$CI_BRANCH" = "cleanup-comind-univ" ]; then - - elpi_CI_REF=expose-comind-univ - elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi - - equations_CI_REF=expose-comind-univ - equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations - - paramcoq_CI_REF=expose-comind-univ - paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq - - mtac2_CI_REF=expose-comind-univ - mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2 - - rewriter_CI_REF=cleanup-comind-univ - rewriter_CI_GITURL=https://github.com/SkySkimmer/rewriter - - -fi diff --git a/dev/ci/user-overlays/11141-herbelin-master+labelled-pr_lconstr-and-co.sh b/dev/ci/user-overlays/11141-herbelin-master+labelled-pr_lconstr-and-co.sh deleted file mode 100644 index fb66217487..0000000000 --- a/dev/ci/user-overlays/11141-herbelin-master+labelled-pr_lconstr-and-co.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11141" ] || [ "$CI_BRANCH" = "master+labelled-pr_lconstr-and-co" ]; then - - quickchick_CI_REF=master+adapt-coq-pr11141 - quickchick_CI_GITURL=https://github.com/herbelin/QuickChick - -fi diff --git a/dev/ci/user-overlays/11172-herbelin-master+coercion-notation-interleaved-printing.sh b/dev/ci/user-overlays/11172-herbelin-master+coercion-notation-interleaved-printing.sh deleted file mode 100644 index e0d9dc6469..0000000000 --- a/dev/ci/user-overlays/11172-herbelin-master+coercion-notation-interleaved-printing.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11172" ] || [ "$CI_BRANCH" = "master+coercion-notation-interleaved-printing" ]; then - - elpi_CI_REF=coq-master+mini-fix-mkGApp - elpi_CI_GITURL=https://github.com/herbelin/coq-elpi - -fi diff --git a/dev/ci/user-overlays/11235-non-maximal-implicit.sh b/dev/ci/user-overlays/11235-non-maximal-implicit.sh deleted file mode 100644 index fd63980036..0000000000 --- a/dev/ci/user-overlays/11235-non-maximal-implicit.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11235" ] || [ "$CI_BRANCH" = "non-maximal-implicit" ]; then - - quickchick_CI_REF=non_maximal_implicit - quickchick_CI_GITURL=https://github.com/SimonBoulier/QuickChick - - elpi_CI_REF=non_maximal_implicit - elpi_CI_GITURL=https://github.com/SimonBoulier/coq-elpi - -fi diff --git a/dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh b/dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh deleted file mode 100644 index a95170a455..0000000000 --- a/dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11293" ] || [ "$CI_BRANCH" = "rename-class-files" ]; then - - elpi_CI_REF=rename-class-files - elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi - - mtac2_CI_REF=rename-class-files - mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 - -fi diff --git a/dev/ci/user-overlays/11338-ppedrot-rm-global-uses-evd.sh b/dev/ci/user-overlays/11338-ppedrot-rm-global-uses-evd.sh deleted file mode 100644 index f41271804a..0000000000 --- a/dev/ci/user-overlays/11338-ppedrot-rm-global-uses-evd.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11338" ] || [ "$CI_BRANCH" = "rm-global-uses-evd" ]; then - - unicoq_CI_REF=rm-global-uses-evd - unicoq_CI_GITURL=https://github.com/ppedrot/unicoq - - equations_CI_REF=rm-global-uses-evd - equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/11368-trailing-implicit-error.sh b/dev/ci/user-overlays/11368-trailing-implicit-error.sh deleted file mode 100644 index a125337dd9..0000000000 --- a/dev/ci/user-overlays/11368-trailing-implicit-error.sh +++ /dev/null @@ -1,33 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11368" ] || [ "$CI_BRANCH" = "trailing_implicit_error" ]; then - - mathcomp_CI_REF=non_maximal_implicit - mathcomp_CI_GITURL=https://github.com/SimonBoulier/math-comp - - oddorder_CI_REF=non_maximal_implicit - oddorder_CI_GITURL=https://github.com/SimonBoulier/odd-order - - stdlib2_CI_REF=non_maximal_implicit - stdlib2_CI_GITURL=https://github.com/SimonBoulier/stdlib2 - - coq_dpdgraph_CI_REF=non_maximal_implicit - coq_dpdgraph_CI_GITURL=https://github.com/SimonBoulier/coq-dpdgraph - - vst_CI_REF=non_maximal_implicit - vst_CI_GITURL=https://github.com/SimonBoulier/VST - - equations_CI_REF=non_maximal_implicit - equations_CI_GITURL=https://github.com/SimonBoulier/Coq-Equations - - mtac2_CI_REF=non_maximal_implicit - mtac2_CI_GITURL=https://github.com/SimonBoulier/Mtac2 - - relation_algebra_CI_REF=non_maximal_implicit - relation_algebra_CI_GITURL=https://github.com/SimonBoulier/relation-algebra - - fiat_parsers_CI_REF=non_maximal_implicit - fiat_parsers_CI_GITURL=https://github.com/SimonBoulier/fiat - - Corn_CI_REF=non_maximal_implicit - Corn_CI_GITURL=https://github.com/SimonBoulier/corn - -fi diff --git a/dev/ci/user-overlays/11417-ppedrot-rm-kind-of-type.sh b/dev/ci/user-overlays/11417-ppedrot-rm-kind-of-type.sh deleted file mode 100644 index 5fb29e1826..0000000000 --- a/dev/ci/user-overlays/11417-ppedrot-rm-kind-of-type.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11417" ] || [ "$CI_BRANCH" = "rm-kind-of-type" ]; then - - elpi_CI_REF=rm-kind-of-type - elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi - -fi diff --git a/dev/ci/user-overlays/11521-SkySkimmer-no-optname.sh b/dev/ci/user-overlays/11521-SkySkimmer-no-optname.sh deleted file mode 100644 index f2a431978d..0000000000 --- a/dev/ci/user-overlays/11521-SkySkimmer-no-optname.sh +++ /dev/null @@ -1,15 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11521" ] || [ "$CI_BRANCH" = "no-optname" ]; then - - coqhammer_CI_REF=no-optname - coqhammer_CI_GITURL=https://github.com/SkySkimmer/coqhammer - - equations_CI_REF=no-optname - equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations - - unicoq_CI_REF=no-optname - unicoq_CI_GITURL=https://github.com/SkySkimmer/unicoq - - paramcoq_CI_REF=no-optname - paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq - -fi diff --git a/dev/ci/user-overlays/11557-SkySkimmer-template-directify.sh b/dev/ci/user-overlays/11557-SkySkimmer-template-directify.sh deleted file mode 100644 index 913b39c30c..0000000000 --- a/dev/ci/user-overlays/11557-SkySkimmer-template-directify.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11557" ] || [ "$CI_BRANCH" = "template-directify" ]; then - - equations_CI_REF=template-directify - equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations - - paramcoq_CI_REF=template-directify - paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq - - elpi_CI_REF=template-directify - elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi - -fi diff --git a/dev/ci/user-overlays/11602-herbelin-master+support-only-parsing-where-clause.sh b/dev/ci/user-overlays/11602-herbelin-master+support-only-parsing-where-clause.sh deleted file mode 100644 index 8b0f86d951..0000000000 --- a/dev/ci/user-overlays/11602-herbelin-master+support-only-parsing-where-clause.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11602" ] || [ "$CI_BRANCH" = "master+support-only-parsing-where-clause" ]; then - - equations_CI_REF=master+adapt-coq-pr11602-only-parsing-where-notation - equations_CI_GITURL=https://github.com/herbelin/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/11708-gares-elpi-1.10.sh b/dev/ci/user-overlays/11708-gares-elpi-1.10.sh deleted file mode 100644 index 121190e5f6..0000000000 --- a/dev/ci/user-overlays/11708-gares-elpi-1.10.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11708" ] || [ "$CI_BRANCH" = " elpi-1.10+coq-elpi-1.3" ]; then - - elpi_CI_REF="coq-master+coq-elpi-1.3" - elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi - -fi diff --git a/dev/ci/user-overlays/11764-ppedrot-simplify-template.sh b/dev/ci/user-overlays/11764-ppedrot-simplify-template.sh deleted file mode 100644 index f8871ae158..0000000000 --- a/dev/ci/user-overlays/11764-ppedrot-simplify-template.sh +++ /dev/null @@ -1,18 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11764" ] || [ "$CI_BRANCH" = "simplify-template" ]; then - - elpi_CI_REF="simplify-template" - elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi - - equations_CI_REF="simplify-template" - equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - - paramcoq_CI_REF="simplify-template" - paramcoq_CI_GITURL=https://github.com/ppedrot/paramcoq - - mtac2_CI_REF="simplify-template" - mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 - - rewriter_CI_REF="simplify-template" - rewriter_CI_GITURL=https://github.com/ppedrot/rewriter - -fi |