Script 'mail_helper' called by obssrc Hello community, here is the log from the commit of package coq for openSUSE:Factory checked in at 2026-03-23 17:13:10 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/coq (Old) and /work/SRC/openSUSE:Factory/.coq.new.8177 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "coq" Mon Mar 23 17:13:10 2026 rev:31 rq:1341905 version:9.1.1 Changes: -------- --- /work/SRC/openSUSE:Factory/coq/coq.changes 2025-01-19 21:49:17.310203093 +0100 +++ /work/SRC/openSUSE:Factory/.coq.new.8177/coq.changes 2026-03-23 17:14:16.559939785 +0100 @@ -1,0 +2,42 @@ +Tue Feb 24 22:14:06 UTC 2026 - Aaron Puchert <[email protected]> + +- Update to version 9.0.0. The most important changes: + * "The Rocq Prover" is the new official name of the project. + * A single rocq binary dispatches commands for compilation, + read-eval-print-loop, documentation building, dependency + computation, etc. + * The Coq standard library has been split into two libraries: + - A Corelib library. This is an extended prelude, which is + enough to run Rocq tactics and contains the Ltac2 library and + bindings for primitive types (integers, floats, arrays and + strings). + - An Stdlib library. The Stdlib is now maintained out of the + main rocq repository. +- The standard library is no longer part of the main package and + has to be installed separately. +- For a detailed change log see + https://rocq-prover.org/doc/v9.0/refman/changes.html#changes-in-9-0-0. +- Update to version 9.1.0. The most important changes: + * Fixed incorrect guard checking leading to inconsistencies. + * Sort polymorphic universe instances should now be written as + `@{s ; u}` instead of `@{s | u}`. + * Fixed handling of notation variables for ltac2 in notations + (i.e. `Notation "'foo' x" := ltac2:(...)`). + * Support for refine attribute in Definition. + * Rocq can be compile-time configured to be relocatable. + * Extraction handles sort polymorphic definitions. +- For a detailed change log see + https://rocq-prover.org/doc/v9.1/refman/changes.html#changes-in-9-1-0. +- Update to version 9.1.1. + * Fixed an anomaly when defining a sort polymorphic inductive + without enabling Universe Polymorphism. + * Compatibility with OCaml 5.4 with warnings as errors. + * Various documentation updates. +- Add translations and magic to MIME types, to distinguish from + other MIME types for the same glob. +- Stop using %suse_update_desktop_file. +- Set license for documentation as Open Publication License v1.0. +- Relax constraints a bit, since we're no longer building the + standard library. + +------------------------------------------------------------------- Old: ---- coq-8.20.1.tar.gz coq-refman-8.20.1.tar.xz coq-stdlib-8.20.1.tar.xz coq.xml fr.inria.coq.coqide.desktop fr.inria.coq.coqide.metainfo.xml New: ---- org.rocq-prover.rocqide.desktop org.rocq-prover.rocqide.metainfo.xml rocq-9.1.1.tar.gz rocq-corelib-doc-9.1.1.tar.xz rocq-refman-9.1.1.tar.xz rocq.xml ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ coq.spec ++++++ --- /var/tmp/diff_new_pack.abXbNZ/_old 2026-03-23 17:14:19.760072877 +0100 +++ /var/tmp/diff_new_pack.abXbNZ/_new 2026-03-23 17:14:19.760072877 +0100 @@ -1,9 +1,8 @@ # # spec file for package coq # -# Copyright (c) 2025 SUSE LLC +# Copyright (c) 2026 SUSE LLC and contributors # Copyright (c) 2012-2018 Peter Trommler, peter.trommler at ohm-hochschule.de -# Copyright (c) 2025 Aaron Puchert <[email protected]> # # All modifications and additions to the file contributed by third parties # remain the property of their copyright owners, unless otherwise agreed @@ -18,33 +17,36 @@ # +# Project has been renamed, but unclear how to rename in OBS. +%global _name rocq + %bcond_without ide -%global dune_packages coq,coq-core,coq-stdlib +%global dune_packages rocq-runtime,rocq-core %if %{with ide} -%global dune_packages %{dune_packages},coqide,coqide-server +%global dune_packages %{dune_packages},rocqide,coqide-server %endif Name: coq -Version: 8.20.1 +Version: 9.1.1 Release: 0 Summary: Proof Assistant based on the Calculus of Inductive Constructions License: LGPL-2.1-only Group: Productivity/Scientific/Math -URL: https://coq.inria.fr/ -Source: https://github.com/coq/coq/archive/V%{version}.tar.gz#/%{name}-%{version}.tar.gz -Source1: fr.inria.coq.coqide.desktop -Source2: fr.inria.coq.coqide.metainfo.xml -Source3: coq.xml -Source50: coq-refman-%{version}.tar.xz -Source51: coq-stdlib-%{version}.tar.xz +URL: https://rocq-prover.org/ +Source: https://github.com/rocq-prover/rocq/archive/V%{version}.tar.gz#/%{_name}-%{version}.tar.gz +Source1: org.rocq-prover.rocqide.desktop +Source2: org.rocq-prover.rocqide.metainfo.xml +Source3: %{_name}.xml +Source50: %{_name}-refman-%{version}.tar.xz +Source51: %{_name}-corelib-doc-%{version}.tar.xz Source100: %{name}-rpmlintrc BuildRequires: desktop-file-utils BuildRequires: fdupes BuildRequires: make >= 3.81 BuildRequires: ocaml >= 4.09.0 BuildRequires: ocaml-camlp5-devel >= 5.08 -BuildRequires: ocaml-dune >= 3.6.1 +BuildRequires: ocaml-dune >= 3.8.3 BuildRequires: ocaml-rpm-macros BuildRequires: ocamlfind(findlib) BuildRequires: ocamlfind(zarith) @@ -55,41 +57,57 @@ Requires: ocamlfind %description +Empty dummy package. + +%package -n %{_name} +Summary: Proof Assistant based on the Calculus of Inductive Constructions +Group: Productivity/Scientific/Math +Provides: coq = %{version}-%{release} +Obsoletes: coq < 9.0.0 + +%description -n %{_name} Proof assistant which allows to handle calculus assertions, check mechanically proofs of these assertions, helps to find formal proofs and extracts a certified program from the constructive proof of its formal specification. This package contains shared files and the command line interface. -For a graphical interface install %{name}-ide. +For a graphical interface install %{_name}-ide. -%package ide +%package -n %{_name}-ide Summary: IDE for The Coq Proof Assistant Group: Productivity/Scientific/Math -Requires: %{name} = %{version} +Requires: %{_name} = %{version} +Provides: coq-ide = %{version}-%{release} +Obsoletes: coq-ide < 9.0.0 -%description ide +%description -n %{_name}-ide The Coq Integrated Development Interface is a graphical interface for the Coq proof assistant. -%package devel +%package -n %{_name}-devel Summary: Development files for coq Group: Development/Libraries/Other -Requires: %{name} = %{version} +Requires: %{_name} = %{version} Requires: ocaml >= 4.09.0 +Provides: coq-devel = %{version}-%{release} +Obsoletes: coq-devel < 9.0.0 -%description devel +%description -n %{_name}-devel This package contains development files for Coq. -%package doc +%package -n %{_name}-doc Summary: Documentation for coq Group: Documentation/HTML -Requires: %{name} = %{version} +License: OPUBL-1.0 +Requires: %{_name} = %{version} +Provides: coq-doc = %{version}-%{release} +Obsoletes: coq-doc < 9.0.0 BuildArch: noarch -%description doc -HTML reference manual for Coq and full documentation of the standard library. +%description -n %{_name}-doc +HTML reference manual for Coq. %prep -%setup -q -a 50 -a 51 +%setup -q -a 50 -a 51 -n %{_name}-%{version} %build %if 0%{?qemu_user_space_build} @@ -109,9 +127,9 @@ -prefix %{_prefix} \ -libdir %{_libdir}/coq \ -mandir %{_mandir} \ - -datadir %{_datadir}/%{name} \ - -docdir %{_docdir}/%{name} \ - -configdir %{_sysconfdir}/xdg/%{name} \ + -datadir %{_datadir}/%{_name} \ + -docdir %{_docdir}/%{_name} \ + -configdir %{_sysconfdir}/xdg/%{_name} \ -native-compiler yes \ -natdynlink yes \ -browser "xdg-open %s" @@ -126,32 +144,18 @@ %ocaml_dune_install %if %{with ide} -%suse_update_desktop_file -i %{SOURCE1} -install -D -m 644 %{SOURCE1} %{buildroot}%{_datadir}/applications/fr.inria.coq.coqide.desktop -install -D -m 644 %{SOURCE2} %{buildroot}%{_datadir}/metainfo/fr.inria.coq.coqide.metainfo.xml -install -D -m 644 %{SOURCE3} %{buildroot}%{_datadir}/mime/packages/coq.xml +install -D -m 644 %{SOURCE1} %{buildroot}%{_datadir}/applications/org.rocq-prover.rocqide.desktop +install -D -m 644 %{SOURCE2} %{buildroot}%{_datadir}/metainfo/org.rocq-prover.rocqide.metainfo.xml +install -D -m 644 %{SOURCE3} %{buildroot}%{_datadir}/mime/packages/rocq.xml mkdir -p %{buildroot}%{_datadir}/icons/hicolor/256x256/apps -ln -s %{_datadir}/coq/coq.png %{buildroot}%{_datadir}/icons/hicolor/256x256/apps/coq.png +ln -s %{_datadir}/coq/coq.png %{buildroot}%{_datadir}/icons/hicolor/256x256/apps/rocq.png %endif -# Sometimes we get identical x and x.opt files, replace by symlink x -> x.opt. -for bin in %{buildroot}%{_bindir}/*.opt -do - if [ -f ${bin%.opt} ] && diff $bin ${bin%.opt} - then - rm ${bin%.opt} - ln -s ${bin#%{buildroot}} ${bin%.opt} - fi -done - # Fix executable bit and shebangs, preferring python3. # (https://www.python.org/dev/peps/pep-0394/#for-python-runtime-distributors) -chmod -x %{buildroot}%{_libdir}/coq-core/tools/TimeFileMaker.py +chmod -x %{buildroot}%{_libdir}/rocq-runtime/tools/TimeFileMaker.py sed -i '1s|^#!/usr/bin/env *|#!/usr/bin/|;1s|^#!/usr/bin/python$|#!/usr/bin/python3|' \ - %{buildroot}%{_libdir}/coq-core/tools/make-{one-time-file,both-{time,single-timing}-files}.py - -# Remove superfluous man page. -rm %{buildroot}%{_mandir}/man1/coqtop.byte.1 + %{buildroot}%{_libdir}/rocq-runtime/tools/make-{one-time-file,both-{time,single-timing}-files}.py # Remove unneeded empty *.vos files. find %{buildroot}%{_libdir}/coq -empty -name '*.vos' -delete @@ -159,7 +163,7 @@ # Build lists of runtime and devel files by ending. # Compiled theories and shared objects are needed at runtime. find %{buildroot}%{_libdir} -type d | sed "s|%{buildroot}|%%dir |g" >dir.list -sed -i '1d; /coq-core\/tools/d' dir.list +sed -i '1d; /rocq-runtime\/tools/d' dir.list find %{buildroot}%{_libdir} -name '*.cmxs' \ -or -name '*.so' \ -or -name '*.vo' | sed "s|%{buildroot}||g" >runtime.list @@ -181,7 +185,7 @@ -or -name '*.v' | sed "s|%{buildroot}||g" >devel.list # Until we can build it, we fetch the documentation from the official website: -# git clone --filter=tree:0 --sparse https://github.com/coq/doc.git +# git clone --filter=tree:0 --sparse https://github.com/rocq-prover/doc.git # pushd doc # git sparse-checkout add V%{version} # cd V%{version} @@ -190,57 +194,46 @@ # -cJf ../../coq-refman-%{version}.tar.xz refman # tar --sort=name --owner=0 --group=0 --mtime="@${SOURCE_DATE_EPOCH}" \ # --pax-option=exthdr.name=%d/PaxHeaders/%f,delete=atime,delete=ctime \ -# -cJf ../../coq-stdlib-%{version}.tar.xz stdlib +# -cJf ../../coq-corelib-doc-%{version}.tar.xz corelib # popd -# Drop some CSS files and headers in stdlib documentation, add some margin directly. -find stdlib/ -name '*.html' -exec sed -i ' -s#//coq.inria.fr/sites/all/themes/coq/coqdoc.css#%{_libdir}/coq-core/tools/coqdoc/coqdoc.css# -/<link type="text\/css" rel="stylesheet" media="all" href="\/\/coq.inria.fr\/.*.css" \/>/d -/<div id="container">/s/>/ style="margin:1em;">/ -/^ <div id="headertop">$/,/^ <\/div>$/d -/^ <div id="header">$/,/^ <\/div>$/d +# Slim down documentation pages, add some margin directly. +find corelib/ -name '*.html' -exec sed -i ' +s#https://rocq-prover\.org/css/stdlib\.css#%{_libdir}/rocq-runtime/tools/coqdoc/coqdoc.css# +/<meta [^h]/d +/<link .* href="https:\/\/rocq-prover\.org.*"/d +/<script defer="".* src=".*"><\/script>/d +/<style>/,/<\/style>/d +/<body/i<body style="margin:1em;"><!-- +/<body/,/END CORELIB HEADER/d +/START CORELIB FOOTER/,/<\/body>/d +/<\/html>/i-->\n</body> ' {} + -mkdir -p %{buildroot}%{_docdir}/%{name} -cp -r refman stdlib %{buildroot}%{_docdir}/%{name} -rm -r %{buildroot}%{_docdir}/%{name}/refman/{.buildinfo,.doctrees,_sources} +mkdir -p %{buildroot}%{_docdir}/%{_name} +cp -r corelib refman %{buildroot}%{_docdir}/%{_name} +rm -r %{buildroot}%{_docdir}/%{_name}/refman/{.buildinfo,.doctrees,_sources} -%fdupes %{buildroot}%{_docdir}/%{name} +%fdupes %{buildroot}%{_docdir}/%{_name} -%files -f dir.list -f runtime.list +%files -n %{_name} -f dir.list -f runtime.list %license LICENSE CREDITS -%{_bindir}/coq-tex -%{_bindir}/coq_makefile -%{_bindir}/coqc -%{_bindir}/coqc.byte -%{_bindir}/coqchk -%{_bindir}/coqdep -%{_bindir}/coqdoc -%{_bindir}/coqnative -%{_bindir}/coqpp -%{_bindir}/coqtimelog2html -%{_bindir}/coqtop -%{_bindir}/coqtop.byte -%{_bindir}/coqwc -%{_bindir}/coqworker.opt -%{_bindir}/coqworkmgr +%{_bindir}/rocq +%{_bindir}/rocq.byte +%{_bindir}/rocqchk %{_bindir}/csdpcert %{_bindir}/ocamllibdep %{_bindir}/votour -%{_libdir}/coq-core/tools -%exclude %{_libdir}/coq-core/tools/CoqMakefile.in +%{_libdir}/rocq-runtime/rocqnative +%{_libdir}/rocq-runtime/rocqworker +%{_libdir}/rocq-runtime/rocqworker.byte +%{_libdir}/rocq-runtime/rocqworker_with_drop +%{_libdir}/rocq-runtime/tools +%exclude %{_libdir}/rocq-runtime/tools/CoqMakefile.in -%{_mandir}/man1/coq-tex.1%{ext_man} -%{_mandir}/man1/coq_makefile.1%{ext_man} -%{_mandir}/man1/coqc.1%{ext_man} -%{_mandir}/man1/coqchk.1%{ext_man} -%{_mandir}/man1/coqdep.1%{ext_man} -%{_mandir}/man1/coqdoc.1%{ext_man} -%{_mandir}/man1/coqnative.1%{ext_man} -%{_mandir}/man1/coqtop.1%{ext_man} -%{_mandir}/man1/coqwc.1%{ext_man} +%{_mandir}/man1/rocq.1%{ext_man} +%{_mandir}/man1/rocqchk.1%{ext_man} %dir %{_datadir}/texmf %dir %{_datadir}/texmf/tex @@ -248,27 +241,28 @@ %dir %{_datadir}/texmf/tex/latex/misc %{_datadir}/texmf/tex/latex/misc/coqdoc.sty +%{_libdir}/{%{dune_packages}}/META + %if %{with ide} -%files ide -%{_bindir}/coqide -%{_bindir}/coqidetop.byte -%{_bindir}/coqidetop.opt -%{_mandir}/man1/coqide.1%{ext_man} -%{_datadir}/%{name} -%{_datadir}/applications/fr.inria.coq.coqide.desktop -%{_datadir}/icons/hicolor/256x256/apps/coq.png -%{_datadir}/metainfo/fr.inria.coq.coqide.metainfo.xml -%{_datadir}/mime/packages/coq.xml +%files -n %{_name}-ide +%{_bindir}/rocqide +%{_bindir}/coqidetop +%{_mandir}/man1/rocqide.1%{ext_man} +%{_datadir}/coq +%{_datadir}/applications/org.rocq-prover.rocqide.desktop +%{_datadir}/icons/hicolor/256x256/apps/rocq.png +%{_datadir}/metainfo/org.rocq-prover.rocqide.metainfo.xml +%{_datadir}/mime/packages/rocq.xml %endif -%files devel -f dir.list -f devel.list -%{_libdir}/coq-core/revision -%{_libdir}/coq-core/dev/ml_toplevel -%{_libdir}/{%{dune_packages}}/{META,dune-package,opam} -%{_libdir}/coq-core/tools/CoqMakefile.in - -%files doc -%dir %{_docdir}/%{name} -%{_docdir}/%{name}/refman -%{_docdir}/%{name}/stdlib +%files -n %{_name}-devel -f dir.list -f devel.list +%{_libdir}/rocq-runtime/revision +%{_libdir}/rocq-runtime/dev/ml_toplevel +%{_libdir}/{%{dune_packages}}/{dune-package,opam} +%{_libdir}/rocq-runtime/tools/CoqMakefile.in + +%files -n %{_name}-doc +%dir %{_docdir}/%{_name} +%{_docdir}/%{_name}/corelib +%{_docdir}/%{_name}/refman ++++++ _constraints ++++++ --- /var/tmp/diff_new_pack.abXbNZ/_old 2026-03-23 17:14:19.800074541 +0100 +++ /var/tmp/diff_new_pack.abXbNZ/_new 2026-03-23 17:14:19.804074708 +0100 @@ -2,7 +2,7 @@ <constraints> <hardware> <memoryperjob> - <size unit="M">900</size> + <size unit="M">600</size> </memoryperjob> <disk> <size unit="G">4</size> ++++++ org.rocq-prover.rocqide.desktop ++++++ [Desktop Entry] Encoding=UTF-8 Type=Application Name=Coq/Rocq IDE GenericName=Proof Assistant Comment=Proof Assistant based on the Calculus of Inductive Constructions Categories=Science;Math; MimeType=text/x-coqsrc; Exec=rocqide %F Icon=rocq ++++++ org.rocq-prover.rocqide.metainfo.xml ++++++ <?xml version="1.0" encoding="UTF-8"?> <component> <id type="desktop">org.rocq-prover.rocqide</id> <metadata_license>CC0-1.0</metadata_license> <name>Coq IDE / RocqIDE</name> <summary>Graphical frontend for the Coq/Rocq formal proof management system</summary> <description> <p> Coq implements a program specification and mathematical higher-level language called <em>Gallina</em> that is based on an expressive formal language called the <em>Calculus of Inductive Constructions</em> that itself combines both a higher-order logic and a richly-typed functional programming language. Through a <em>vernacular</em> language of commands, Coq allows: </p> <ul> <li>to define functions or predicates, that can be evaluated efficiently;</li> <li>to state mathematical theorems and software specifications;</li> <li>to interactively develop formal proofs of these theorems;</li> <li>to machine-check these proofs by a relatively small certification "kernel";</li> <li>to extract certified programs to languages like OCaml, Haskell or Scheme.</li> </ul> <p> As a proof development system, Coq provides interactive proof methods, decision and semi-decision algorithms, and a <em>tactic</em> language for letting the user define its own proof methods. Connection with external computer algebra system or theorem provers is available. </p> <p> As a platform for the formalization of mathematics or the development of programs, Coq provides support for high-level notations, implicit contents and various other useful kinds of macros. </p> </description> <categories> <category>Development</category> <category>IDE</category> <category>Science</category> <category>ComputerScience</category> <category>Math</category> </categories> <keywords> <keyword>dependent-types</keyword> <keyword>theorem-proving</keyword> <keyword>proof-assistant</keyword> </keywords> <url type="homepage">https://rocq-prover.org/</url> <url type="bugtracker">https://github.com/rocq-prover/rocq/issues</url> <url type="faq">https://github.com/rocq-prover/rocq/wiki/The-Rocq-FAQ</url> <url type="help">https://rocq-prover.org/refman/practical-tools/coqide.html</url> <url type="donation">https://rocq-prover.org/consortium</url> <url type="vcs-browser">https://github.com/rocq-prover/rocq</url> <url type="contribute">https://github.com/rocq-prover/rocq/blob/master/CONTRIBUTING.md</url> <launchable type="desktop-id">org.rocq-prover.rocqide.desktop</launchable> <releases> <release version="9.1.1" date="2026-02-09"/> <release version="9.1.0" date="2025-09-15"/> <release version="9.0.0" date="2025-03-12"/> <release version="8.20.1" date="2025-01-16"/> <release version="8.20.0" date="2024-09-04"/> <release version="8.19.1" date="2024-03-04"/> <release version="8.19.0" date="2024-01-24"/> <release version="8.18.0" date="2023-09-08"/> <release version="8.17.1" date="2023-06-27"/> <release version="8.17.0" date="2023-03-27"/> <release version="8.16.1" date="2022-11-25"/> <release version="8.16.0" date="2022-09-05"/> <release version="8.15.2" date="2022-05-31"/> <release version="8.15.1" date="2022-03-22"/> </releases> <provides> <binary>coqide</binary> </provides> <project_license>LGPL-2.1-only</project_license> <screenshots> <screenshot type="default"> <image type="source"> https://rocq-prover.org/refman/_images/rocqide.png </image> </screenshot> </screenshots> <content_rating type="oars-1.1"/> </component> ++++++ rocq.xml ++++++ <?xml version="1.0" encoding="UTF-8"?> <mime-info xmlns="http://www.freedesktop.org/standards/shared-mime-info";> <mime-type type="text/x-coqsrc"> <comment>Coq/Rocq source code</comment> <!-- Translations stolen from other source code types --> <comment xml:lang="zh-Hant-TW">Coq/Rocq 源碼</comment> <comment xml:lang="zh-Hans-CN">Coq/Rocq 源代码</comment> <comment xml:lang="vi">Mã nguồn Coq/Rocq</comment> <comment xml:lang="uk">початковий код мовою Coq/Rocq</comment> <comment xml:lang="tr">Coq/Rocq kaynak kodu</comment> <comment xml:lang="sv">Coq/Rocq-källkod</comment> <comment xml:lang="sq">kod burim Coq/Rocq</comment> <comment xml:lang="sl">Datoteka izvorne kode Coq/Rocq</comment> <comment xml:lang="si">Coq/Rocq මූල කේතය</comment> <comment xml:lang="sk">Zdrojový kód jazyka Coq/Rocq</comment> <comment xml:lang="ru">Исходный код Coq/Rocq</comment> <comment xml:lang="ro">Cod sursă Coq/Rocq</comment> <comment xml:lang="pt-BR">Código-fonte Coq/Rocq</comment> <comment xml:lang="pt">código origem Coq/Rocq</comment> <comment xml:lang="pl">Kod źródłowy Coq/Rocq</comment> <comment xml:lang="oc">còde font Coq/Rocq</comment> <comment xml:lang="nn">Coq/Rocq-kjeldekode</comment> <comment xml:lang="nl">Coq/Rocq-broncode</comment> <comment xml:lang="nb">Coq/Rocq-kildekode</comment> <comment xml:lang="ms">Kod sumber Coq/Rocq</comment> <comment xml:lang="lv">Coq/Rocq pirmkods</comment> <comment xml:lang="lt">Coq/Rocq pradinis kodas</comment> <comment xml:lang="ko">Coq/Rocq 소스 코드</comment> <comment xml:lang="kk-Cyrl">Coq/Rocq бастапқы коды</comment> <comment xml:lang="ka">Coq/Rocq-ის საწყისი კოდი</comment> <comment xml:lang="ja">Coq/Rocq ソースコード</comment> <comment xml:lang="it">Codice sorgente Coq/Rocq</comment> <comment xml:lang="is">Coq/Rocq frumkóði</comment> <comment xml:lang="id">Kode sumber Coq/Rocq</comment> <comment xml:lang="ia">Codice-fonte Coq/Rocq</comment> <comment xml:lang="hu">Coq/Rocq-forráskód</comment> <comment xml:lang="hr">Coq/Rocq izvorni kôd</comment> <comment xml:lang="he">קוד מקור של Coq/Rocq</comment> <comment xml:lang="gl">código fonte de Coq/Rocq</comment> <comment xml:lang="ga">cód foinseach Coq/Rocq</comment> <comment xml:lang="fur">codiç sorzint Coq/Rocq</comment> <comment xml:lang="fr">code source Coq/Rocq</comment> <comment xml:lang="fo">Coq/Rocq keldukota</comment> <comment xml:lang="fi">Coq/Rocq-lähdekoodi</comment> <comment xml:lang="eu">Coq/Rocq iturburu-kodea</comment> <comment xml:lang="es">código fuente en Coq/Rocq</comment> <comment xml:lang="eo">Coq/Rocq-fontkodo</comment> <comment xml:lang="en-GB">Coq/Rocq source code</comment> <comment xml:lang="el">Πηγαίος κώδικας Coq/Rocq</comment> <comment xml:lang="de">Coq/Rocq-Quelltext</comment> <comment xml:lang="da">Coq/Rocq-kildekode</comment> <comment xml:lang="cs">zdrojový kód v jazyce Coq/Rocq</comment> <comment xml:lang="ca">codi font en Coq/Rocq</comment> <comment xml:lang="bg">Изходен код — Coq/Rocq</comment> <comment xml:lang="be-Latn">Kryničny kod Coq/Rocq</comment> <comment xml:lang="be-Cyrl">зыходны код Coq/Rocq</comment> <comment xml:lang="ar">شفرة مصدر Coq/Rocq</comment> <comment xml:lang="af">Coq/Rocq-bronkode</comment> <glob pattern="*.v"/> <!-- To distinguish from Verilog, which has the same file ending. --> <magic> <match type="string" offset="0" value="(*"/> <match type="string" offset="0:31" value="Require"/> </magic> <icon name="rocq"/> </mime-type> <mime-type type="application/x-coq-object"> <comment>Coq/Rocq object code</comment> <!-- Translations stolen from object code type --> <comment xml:lang="uk">об'єктний код Coq/Rocq</comment> <comment xml:lang="sv">Coq/Rocq-objektkod</comment> <comment xml:lang="ru">Объектный код Coq/Rocq</comment> <comment xml:lang="pl">Kod obiektowy Coq/Rocq</comment> <comment xml:lang="ja">Coq/Rocq 目的符号文書</comment> <comment xml:lang="it">Codice oggetto Coq/Rocq</comment> <comment xml:lang="gl">Código obxecto de Coq/Rocq</comment> <comment xml:lang="eu">Coq/Rocq Objektu-kodea</comment> <comment xml:lang="es">código de objeto en Coq/Rocq</comment> <comment xml:lang="de">Coq/Rocq-Objektcode</comment> <glob pattern="*.vo"/> </mime-type> </mime-info>
