Merge PR coq#17510: Remove old overlay files

Reviewed-by: Alizter Co-authored-by: Alizter <Alizter@users.noreply.github.com>
Zimmi48 · Apr 19, 2023 · 9368fc2 · 9368fc2
2 parents fbdc9d9 + 6e942ff
commit 9368fc2
Show file tree

Hide file tree

Showing 99 changed files with 0 additions and 341 deletions.
diff --git a/dev/ci/user-overlays/13448-gares-fix_simpl_never_wrt_delta.sh b/dev/ci/user-overlays/13448-gares-fix_simpl_never_wrt_delta.sh
diff --git a/dev/ci/user-overlays/13448-ybertot-fix_simpl_never_wrt_delta.sh b/dev/ci/user-overlays/13448-ybertot-fix_simpl_never_wrt_delta.sh
diff --git a/dev/ci/user-overlays/13965-gares-syndef-principal-scope.sh b/dev/ci/user-overlays/13965-gares-syndef-principal-scope.sh
diff --git a/dev/ci/user-overlays/13969-mattam82-rewrite-reflexive-mode.sh b/dev/ci/user-overlays/13969-mattam82-rewrite-reflexive-mode.sh
diff --git a/dev/ci/user-overlays/14137-alizter-setoid-rewrite-type.sh b/dev/ci/user-overlays/14137-alizter-setoid-rewrite-type.sh
diff --git a/dev/ci/user-overlays/14563-herbelin-master+record-with-default-variable-name.sh b/dev/ci/user-overlays/14563-herbelin-master+record-with-default-variable-name.sh
diff --git a/dev/ci/user-overlays/14727-herbelin-master+major-refactoring-cooking.sh b/dev/ci/user-overlays/14727-herbelin-master+major-refactoring-cooking.sh
diff --git a/dev/ci/user-overlays/14740-alizter-alizter+split-scheme-vernac.sh b/dev/ci/user-overlays/14740-alizter-alizter+split-scheme-vernac.sh
diff --git a/dev/ci/user-overlays/15220-gares-dynlink-w-findlib.sh b/dev/ci/user-overlays/15220-gares-dynlink-w-findlib.sh
diff --git a/dev/ci/user-overlays/15233-SkySkimmer-locality.sh b/dev/ci/user-overlays/15233-SkySkimmer-locality.sh
diff --git a/dev/ci/user-overlays/15274-SkySkimmer-tacopt.sh b/dev/ci/user-overlays/15274-SkySkimmer-tacopt.sh
diff --git a/dev/ci/user-overlays/15294-Lysxia-extract-comparison.sh b/dev/ci/user-overlays/15294-Lysxia-extract-comparison.sh
diff --git a/dev/ci/user-overlays/15317-SkySkimmer-libobject-names.sh b/dev/ci/user-overlays/15317-SkySkimmer-libobject-names.sh
diff --git a/dev/ci/user-overlays/15324-ppedrot-rm-eauto-bfs-implem.sh b/dev/ci/user-overlays/15324-ppedrot-rm-eauto-bfs-implem.sh
diff --git a/dev/ci/user-overlays/15327-ppedrot-split-tclfail-level.sh b/dev/ci/user-overlays/15327-ppedrot-split-tclfail-level.sh
diff --git a/dev/ci/user-overlays/15344-herbelin-master+renaming-syntax_def.ml-abbreviation.ml.sh b/dev/ci/user-overlays/15344-herbelin-master+renaming-syntax_def.ml-abbreviation.ml.sh
diff --git a/dev/ci/user-overlays/15344-herbelin-renaming-syntax_def.ml-abbreviation.ml.sh b/dev/ci/user-overlays/15344-herbelin-renaming-syntax_def.ml-abbreviation.ml.sh
diff --git a/dev/ci/user-overlays/15393-ppedrot-deprecate-sigma-wrapper.sh b/dev/ci/user-overlays/15393-ppedrot-deprecate-sigma-wrapper.sh
diff --git a/dev/ci/user-overlays/15407-ppedrot-evarutil-precise-naming-mode.sh b/dev/ci/user-overlays/15407-ppedrot-evarutil-precise-naming-mode.sh
diff --git a/dev/ci/user-overlays/15414-ppedrot-reduce-global-use.sh b/dev/ci/user-overlays/15414-ppedrot-reduce-global-use.sh
diff --git a/...r-overlays/15420-herbelin-master+fix15420-hardwire-names-pred-mutual-induction-schemes.sh b/...r-overlays/15420-herbelin-master+fix15420-hardwire-names-pred-mutual-induction-schemes.sh
diff --git a/dev/ci/user-overlays/15446-olaure01-signatureT.sh b/dev/ci/user-overlays/15446-olaure01-signatureT.sh
diff --git a/dev/ci/user-overlays/15565-herbelin-master+it_mkLambda-and-cie-econstr-termops-dispatch.sh b/dev/ci/user-overlays/15565-herbelin-master+it_mkLambda-and-cie-econstr-termops-dispatch.sh
diff --git a/dev/ci/user-overlays/15582-herbelin-master+cleaning-decompose_lam_n_assum-and-cie.sh b/dev/ci/user-overlays/15582-herbelin-master+cleaning-decompose_lam_n_assum-and-cie.sh
diff --git a/dev/ci/user-overlays/15638-gares-fix-findlib-pack-rule.sh b/dev/ci/user-overlays/15638-gares-fix-findlib-pack-rule.sh
diff --git a/dev/ci/user-overlays/15645-alizter-alizter+improve-coqide-help.sh b/dev/ci/user-overlays/15645-alizter-alizter+improve-coqide-help.sh
diff --git a/dev/ci/user-overlays/15650-LPCIC-external-dependency.sh b/dev/ci/user-overlays/15650-LPCIC-external-dependency.sh
diff --git a/dev/ci/user-overlays/15656-gares-bump-elpi.sh b/dev/ci/user-overlays/15656-gares-bump-elpi.sh
diff --git a/dev/ci/user-overlays/15693-gares-reverse-coercions.sh b/dev/ci/user-overlays/15693-gares-reverse-coercions.sh
diff --git a/dev/ci/user-overlays/15721-fajb-micromega-interval-analysis.sh b/dev/ci/user-overlays/15721-fajb-micromega-interval-analysis.sh
diff --git a/dev/ci/user-overlays/15807-SkySkimmer-delayed_univs.sh b/dev/ci/user-overlays/15807-SkySkimmer-delayed_univs.sh
diff --git a/dev/ci/user-overlays/15836-proux01-doc_inductive.sh b/dev/ci/user-overlays/15836-proux01-doc_inductive.sh
diff --git a/dev/ci/user-overlays/15837-ppedrot-reduce-universe-footprint.sh b/dev/ci/user-overlays/15837-ppedrot-reduce-universe-footprint.sh
diff --git a/dev/ci/user-overlays/15853-proux01-nonuniform_attr.sh b/dev/ci/user-overlays/15853-proux01-nonuniform_attr.sh
diff --git a/dev/ci/user-overlays/15856-ppedrot-universes-rm-univ-of-sort.sh b/dev/ci/user-overlays/15856-ppedrot-universes-rm-univ-of-sort.sh
diff --git a/dev/ci/user-overlays/15867-SkySkimmer-edge-4.14.sh b/dev/ci/user-overlays/15867-SkySkimmer-edge-4.14.sh
diff --git a/dev/ci/user-overlays/15871-ppedrot-univ-cleanup-api.sh b/dev/ci/user-overlays/15871-ppedrot-univ-cleanup-api.sh
diff --git a/dev/ci/user-overlays/15872-gares-interp-inductive.sh b/dev/ci/user-overlays/15872-gares-interp-inductive.sh
diff --git a/dev/ci/user-overlays/15877-proux01-cleanup_class_record.sh b/dev/ci/user-overlays/15877-proux01-cleanup_class_record.sh
diff --git a/dev/ci/user-overlays/15880-blaisorblade-coq_mk-delete-on-err.sh b/dev/ci/user-overlays/15880-blaisorblade-coq_mk-delete-on-err.sh
diff --git a/dev/ci/user-overlays/15884-proux01-num_not_no_elab.sh b/dev/ci/user-overlays/15884-proux01-num_not_no_elab.sh
diff --git a/dev/ci/user-overlays/15915-ppedrot-pattern-of-constr-nf-flag.sh b/dev/ci/user-overlays/15915-ppedrot-pattern-of-constr-nf-flag.sh
diff --git a/dev/ci/user-overlays/15943-ppedrot-cache-projection-relevance.sh b/dev/ci/user-overlays/15943-ppedrot-cache-projection-relevance.sh
diff --git a/dev/ci/user-overlays/15945-SkySkimmer-require-filters.sh b/dev/ci/user-overlays/15945-SkySkimmer-require-filters.sh
diff --git a/dev/ci/user-overlays/15948-gares-bump-elpi.sh b/dev/ci/user-overlays/15948-gares-bump-elpi.sh
diff --git a/dev/ci/user-overlays/16039-ppedrot-rm-legacy-tactic-engine.sh b/dev/ci/user-overlays/16039-ppedrot-rm-legacy-tactic-engine.sh
diff --git a/dev/ci/user-overlays/16206-extraction-less-recurse.sh b/dev/ci/user-overlays/16206-extraction-less-recurse.sh
diff --git a/dev/ci/user-overlays/16207-SkySkimmer-rm-depr-globref.sh b/dev/ci/user-overlays/16207-SkySkimmer-rm-depr-globref.sh
diff --git a/dev/ci/user-overlays/16230-proux01-field_instance.sh b/dev/ci/user-overlays/16230-proux01-field_instance.sh
diff --git a/dev/ci/user-overlays/16300-SkySkimmer-noiter.sh b/dev/ci/user-overlays/16300-SkySkimmer-noiter.sh
diff --git a/dev/ci/user-overlays/16328-gares-declare-export-seff.sh b/dev/ci/user-overlays/16328-gares-declare-export-seff.sh
diff --git a/dev/ci/user-overlays/16337-ppedrot-clean-autorewrite-db.sh b/dev/ci/user-overlays/16337-ppedrot-clean-autorewrite-db.sh
diff --git a/dev/ci/user-overlays/16344-gares-update-elpi.sh b/dev/ci/user-overlays/16344-gares-update-elpi.sh
diff --git a/dev/ci/user-overlays/16434-SkySkimmer-assumptions-vos.sh b/dev/ci/user-overlays/16434-SkySkimmer-assumptions-vos.sh
diff --git a/dev/ci/user-overlays/16442-ppedrot-evar-compact-instance.sh b/dev/ci/user-overlays/16442-ppedrot-evar-compact-instance.sh
diff --git a/dev/ci/user-overlays/16472-proux01-argument_multiple_scopes.sh b/dev/ci/user-overlays/16472-proux01-argument_multiple_scopes.sh
diff --git a/dev/ci/user-overlays/16488-ppedrot-stricter-evar-access.sh b/dev/ci/user-overlays/16488-ppedrot-stricter-evar-access.sh
diff --git a/dev/ci/user-overlays/16641-ppedrot-typeops-no-case-expand.sh b/dev/ci/user-overlays/16641-ppedrot-typeops-no-case-expand.sh
diff --git a/dev/ci/user-overlays/16682-alizter-master.sh b/dev/ci/user-overlays/16682-alizter-master.sh
diff --git a/dev/ci/user-overlays/16743-SkySkimmer-refreeze.sh b/dev/ci/user-overlays/16743-SkySkimmer-refreeze.sh
diff --git a/dev/ci/user-overlays/16773-ppedrot-factorize-evar-tactics.sh b/dev/ci/user-overlays/16773-ppedrot-factorize-evar-tactics.sh
diff --git a/dev/ci/user-overlays/16858-SkySkimmer-revert-broken-fiat.sh b/dev/ci/user-overlays/16858-SkySkimmer-revert-broken-fiat.sh
diff --git a/dev/ci/user-overlays/16897-gares-fix-tac-j-0.sh b/dev/ci/user-overlays/16897-gares-fix-tac-j-0.sh
diff --git a/dev/ci/user-overlays/16903-ppedrot-sort-poly-stub.sh b/dev/ci/user-overlays/16903-ppedrot-sort-poly-stub.sh
diff --git a/dev/ci/user-overlays/16930-SkySkimmer-flag-native.sh b/dev/ci/user-overlays/16930-SkySkimmer-flag-native.sh
diff --git a/dev/ci/user-overlays/16933-ppedrot-esorts-respect-api.sh b/dev/ci/user-overlays/16933-ppedrot-esorts-respect-api.sh
diff --git a/dev/ci/user-overlays/16935-herbelin-master+functional-strict_check.sh b/dev/ci/user-overlays/16935-herbelin-master+functional-strict_check.sh
diff --git a/...37-herbelin-master+fix12467-inconsistent-convention-mixed-binderlist-termlist-notation.sh b/...37-herbelin-master+fix12467-inconsistent-convention-mixed-binderlist-termlist-notation.sh
diff --git a/dev/ci/user-overlays/16938-SkySkimmer-staged-options.sh b/dev/ci/user-overlays/16938-SkySkimmer-staged-options.sh
diff --git a/dev/ci/user-overlays/16944-maximedenes-separate-notation-syntax.sh b/dev/ci/user-overlays/16944-maximedenes-separate-notation-syntax.sh
diff --git a/dev/ci/user-overlays/16958-SkySkimmer-no-lazy-val.sh b/dev/ci/user-overlays/16958-SkySkimmer-no-lazy-val.sh
diff --git a/dev/ci/user-overlays/16960-SkySkimmer-rm-unsafe-occur-metaevar.sh b/dev/ci/user-overlays/16960-SkySkimmer-rm-unsafe-occur-metaevar.sh
diff --git a/dev/ci/user-overlays/16981-jfehrle-fix_proof_mode.sh b/dev/ci/user-overlays/16981-jfehrle-fix_proof_mode.sh
diff --git a/dev/ci/user-overlays/16992-SkySkimmer-volatile-cast.sh b/dev/ci/user-overlays/16992-SkySkimmer-volatile-cast.sh
diff --git a/dev/ci/user-overlays/17007-ppedrot-module-alg-compact.sh b/dev/ci/user-overlays/17007-ppedrot-module-alg-compact.sh
diff --git a/dev/ci/user-overlays/17016-SkySkimmer-explain-serapi.sh b/dev/ci/user-overlays/17016-SkySkimmer-explain-serapi.sh
diff --git a/dev/ci/user-overlays/17021-andres-erbsen-DecidableClass-instances.sh b/dev/ci/user-overlays/17021-andres-erbsen-DecidableClass-instances.sh
diff --git a/dev/ci/user-overlays/17035-SkySkimmer-no-hresolve.sh b/dev/ci/user-overlays/17035-SkySkimmer-no-hresolve.sh
diff --git a/dev/ci/user-overlays/17038-palmskog-drop-rectypes-coq_makefile.sh b/dev/ci/user-overlays/17038-palmskog-drop-rectypes-coq_makefile.sh
diff --git a/dev/ci/user-overlays/17049-ppedrot-module-expr-compact.sh b/dev/ci/user-overlays/17049-ppedrot-module-expr-compact.sh
diff --git a/dev/ci/user-overlays/17053-ppedrot-classify-evar-find-type.sh b/dev/ci/user-overlays/17053-ppedrot-classify-evar-find-type.sh
diff --git a/dev/ci/user-overlays/17091-ppedrot-cclosure-relevance-quality-var.sh b/dev/ci/user-overlays/17091-ppedrot-cclosure-relevance-quality-var.sh
diff --git a/dev/ci/user-overlays/17096-SkySkimmer-detyping-flgs.sh b/dev/ci/user-overlays/17096-SkySkimmer-detyping-flgs.sh
diff --git a/dev/ci/user-overlays/17098-SkySkimmer-gramlib-functional.sh b/dev/ci/user-overlays/17098-SkySkimmer-gramlib-functional.sh
diff --git a/dev/ci/user-overlays/17177-SkySkimmer-prlev.sh b/dev/ci/user-overlays/17177-SkySkimmer-prlev.sh
diff --git a/dev/ci/user-overlays/17194-ppedrot-quotient-upper-layer-canord-names.sh b/dev/ci/user-overlays/17194-ppedrot-quotient-upper-layer-canord-names.sh
diff --git a/dev/ci/user-overlays/17220-SkySkimmer-pgenarg.sh b/dev/ci/user-overlays/17220-SkySkimmer-pgenarg.sh
diff --git a/dev/ci/user-overlays/17265-SkySkimmer-find-map.sh b/dev/ci/user-overlays/17265-SkySkimmer-find-map.sh
diff --git a/dev/ci/user-overlays/17274-SkySkimmer-check-eval.sh b/dev/ci/user-overlays/17274-SkySkimmer-check-eval.sh