coq.spec

   1 #
   2 # Conditional build:
   3 %bcond_without  ocaml_opt       # native optimized binaries (bytecode is always built)
   4 %bcond_with     sse2            # SSE2 instructions
   5 %bcond_with     doc             # documentation
   6 %bcond_with     tests           # run testsuite (csdp dependant micromega tests fail badly on x86_64)
   7 #
   8 %ifarch pentium4 %{x8664} x32
   9 %define         with_sse2       1
  10 %endif
  11
  12 %ifnarch %{ix86} %{x8664} %{arm} aarch64 ppc sparc sparcv9
  13 %undefine       with_ocaml_opt
  14 %endif
  15
  16 Summary:        The Coq Proof Assistant
  17 Summary(pl.UTF-8):      Coq - narzędzie pomagające w udowadnianiu
  18 Name:           coq
  19 Version:        8.15.0
  20 Release:        1
  21 License:        LGPL v2.1
  22 Group:          Applications/Math
  23 #Source0Download: https://github.com/coq/coq/releases
  24 Source0:        https://github.com/coq/coq/archive/V%{version}/%{name}-%{version}.tar.gz
  25 # Source0-md5:  cfa91d270e013b0ebe49120c2101d010
  26 Source1:        coqide.desktop
  27 Source2:        coqide.xpm
  28 Patch0:         %{name}-dune-prefix.patch
  29 URL:            https://coq.inria.fr/
  30 BuildRequires:  bash
  31 BuildRequires:  ocaml >= 1:4.05
  32 BuildRequires:  camlp5 >= 5.01
  33 BuildRequires:  ocaml-dune >= 2.5.0
  34 BuildRequires:  ocaml-findlib >= 1.8.1
  35 BuildRequires:  ocaml-zarith-devel >= 1.10
  36 BuildRequires:  ocaml-lablgtk3-devel >= 3.1.0
  37 BuildRequires:  ocaml-lablgtk3-gtksourceview-devel >= 3.1.0
  38 BuildRequires:  sed >= 4.0
  39 %if %{with doc}
  40 BuildRequires:  python3 >= 1:3
  41 # TODO (and adjust package name)
  42 BuildRequires:  python3-antlr4-python3-runtime >= 4.7.1
  43 BuildRequires:  python3-bs4 >= 4.0.6
  44 BuildRequires:  python3-pexpect >= 4.2.1
  45 BuildRequires:  python3-sphinx_rtd_theme >= 0.4.3
  46 # TODO (and adjust package name)
  47 BuildRequires:  python3-sphinxcontrib-bibtex >= 0.4.2
  48 BuildRequires:  sphinx-pdg >= 2.3.1
  49 # TODO: update texlive packages list (or drop pdf building leaving only html)
  50 BuildRequires:  texlive-fonts-cmextra
  51 BuildRequires:  texlive-fonts-cmsuper
  52 BuildRequires:  texlive-fonts-other
  53 BuildRequires:  texlive-format-pdflatex
  54 BuildRequires:  texlive-latex-ams
  55 BuildRequires:  texlive-latex-comment
  56 BuildRequires:  texlive-latex-moreverb
  57 BuildRequires:  texlive-latex-ucs
  58 BuildRequires:  texlive-makeindex
  59 BuildRequires:  texlive-psutils
  60 # hyperref.sty (from latex) requires ifxexex.sty (from xetex)
  61 BuildRequires:  texlive-xetex
  62 %endif
  63 %if %{with sse2}
  64 Requires:       cpuinfo(sse2)
  65 %endif
  66 Requires:       ocaml-coq-devel = %{version}-%{release}
  67 Obsoletes:      coq-emacs < 8.13.1
  68 # same as ocaml-zarith
  69 ExclusiveArch:  %{ix86} %{x8664} %{arm} aarch64 ppc sparc sparcv9
  70 BuildRoot:      %{tmpdir}/%{name}-%{version}-root-%(id -u -n)
  71
  72 # Exclude private ocaml interfaces
  73 %define         _noautoreq      ocamlx?\\\((Configwin_types|Interface|Richpp|Serialize|Xml_p(arser|rinter)|Xmlprotocol)\\\)
  74
  75 %description
  76 Coq is a proof assistant which:
  77  - allows to handle calculus assertions,
  78  - check mechanically proofs of these assertions,
  79  - helps to find formal proofs,
  80  - extracts a certified program from the constructive proof of its
  81    formal specification.
  82
  83 %description -l pl.UTF-8
  84 Coq to narzędzie pomagające w udowadnianiu, które:
  85 - pozwala uporać się z twierdzeniami dotyczącymi rachunku
  86   różniczkowego,
  87 - mechanicznie sprawdzać dowody tych twierdzeń,
  88 - pomagać w znalezieniu formalnych dowodów,
  89 - wyciągać program o dowiedzionej poprawności z konstruktywnego dowodu
  90   jego formalnej specyfikacji.
  91
  92 %package -n ocaml-coq
  93 Summary:        Coq Proof Assistant - OCaml runtime libraries
  94 Summary(pl.UTF-8):      Asystent udowadniania Coq - biblioteki uruchomieniowe OCamla
  95 Group:          Libraries
  96 %requires_eq    ocaml-runtime
  97
  98 %description -n ocaml-coq
  99 Coq Proof Assistant - OCaml runtime libraries.
 100
 101 %description -n ocaml-coq -l pl.UTF-8
 102 Asystent udowadniania Coq - biblioteki uruchomieniowe OCamla.
 103
 104 %package -n ocaml-coq-devel
 105 Summary:        Coq Proof Assistant - OCaml development libraries
 106 Summary(pl.UTF-8):      Asystent udowadniania Coq - biblioteki programistyczne OCamla
 107 Group:          Development/Libraries
 108 Requires:       ocaml-coq = %{version}-%{release}
 109 %requires_eq    ocaml
 110
 111 %description -n ocaml-coq-devel
 112 Coq Proof Assistant - OCaml development libraries.
 113
 114 %description -n ocaml-coq-devel -l pl.UTF-8
 115 Asystent udowadniania Coq - biblioteki programistyczne OCamla.
 116
 117 %package latex
 118 Summary:        Coq documentation style for LaTeX
 119 Summary(pl.UTF-8):      Styl dokumentacji Coq dla LaTeXa
 120 Group:          Development/Tools
 121 Requires:       %{name} = %{version}-%{release}
 122
 123 %description latex
 124 Coq documentation style for LaTeX.
 125
 126 %description latex -l pl.UTF-8
 127 Styl dokumentacji Coq dla LaTeXa.
 128
 129 %prep
 130 %setup -q
 131 %patch0 -p1
 132
 133 %{__sed} -i 's|-Wall.*-O2|%{rpmcflags} -Wno-unused|' tools/configure/configure.ml
 134 %if %{with sse2}
 135 %{__sed} -i -e '/cflags_sse2/ s/-msse2 -mfpmath=sse//' configure.ml
 136 %endif
 137 %{__sed} -i 's,-shared,& -g,g' tools/CoqMakefile.in
 138
 139 %{__sed} -i -e '1s,/usr/bin/env python3,%{__python3},' \
 140       tools/make-both-single-timing-files.py \
 141       tools/make-both-time-files.py \
 142       tools/make-one-time-file.py
 143
 144 %{__sed} -i -e '1s,/usr/bin/env python2,%{__python3},' \
 145       doc/tools/coqrst/notations/fontsupport.py
 146
 147 %build
 148 ./configure \
 149         -prefix %{_prefix} \
 150         -configdir %{_sysconfdir}/%{name} \
 151         -datadir %{_datadir}/%{name} \
 152         -docdir %{_docdir}/%{name}-%{version} \
 153         -libdir %{_libdir}/coq \
 154         -mandir %{_mandir} \
 155 %if %{with ocaml_opt}
 156         -coqide opt \
 157         -native-compiler yes \
 158 %else
 159         -byte-only \
 160         -coqide byte \
 161         -native-compiler no \
 162 %endif
 163         -browser "xdg-open %s" \
 164         %{?with_doc:-with-doc yes}
 165
 166 %{__make} world \
 167         CAML_LD_LIBRARY_PATH=kernel/byterun \
 168         _DDISPLAY=verbose \
 169         VERBOSE=1
 170 %{?with_tests:%{__make} check VERBOSE=1 CAML_LD_LIBRARY_PATH=kernel/byterun} # Use native coq to compile theories
 171
 172 %install
 173 rm -rf $RPM_BUILD_ROOT
 174 install -d $RPM_BUILD_ROOT{%{_desktopdir},%{_pixmapsdir},%{_sysconfdir}/%{name}}
 175
 176 %{__make} install \
 177         _DDISPLAY=verbose \
 178         DESTDIR=$RPM_BUILD_ROOT
 179
 180 cp -p %{SOURCE1} $RPM_BUILD_ROOT%{_desktopdir}
 181 cp -p %{SOURCE2} $RPM_BUILD_ROOT%{_pixmapsdir}
 182
 183 cp -p CREDITS README.md $RPM_BUILD_ROOT%{_docdir}/%{name}-%{version}
 184
 185 %{__rm} $RPM_BUILD_ROOT%{_libdir}/ocaml/coq-core/*/*.ml
 186 %{__rm} $RPM_BUILD_ROOT%{_libdir}/ocaml/coq-core/*/*/*.ml
 187 %{__rm} $RPM_BUILD_ROOT%{_libdir}/ocaml/coq-core/*/*/*/*.ml
 188 %{__rm} $RPM_BUILD_ROOT%{_libdir}/ocaml/coqide-server/*/*.ml
 189 # build time
 190 %{__rm} -r $RPM_BUILD_ROOT%{_libdir}/ocaml/coq-core/tools
 191
 192 %clean
 193 rm -rf $RPM_BUILD_ROOT
 194
 195 %files
 196 %defattr(644,root,root,755)
 197 %doc %{_docdir}/%{name}-%{version}
 198 %dir %{_sysconfdir}/%{name}
 199 %attr(755,root,root) %{_bindir}/coq-tex
 200 %attr(755,root,root) %{_bindir}/coq_makefile
 201 %attr(755,root,root) %{_bindir}/coqc
 202 %attr(755,root,root) %{_bindir}/coqc.byte
 203 %attr(755,root,root) %{_bindir}/coqchk
 204 %attr(755,root,root) %{_bindir}/coqdep
 205 %attr(755,root,root) %{_bindir}/coqdoc
 206 %attr(755,root,root) %{_bindir}/coqide
 207 %attr(755,root,root) %{_bindir}/coqidetop.byte
 208 %attr(755,root,root) %{_bindir}/coqidetop.opt
 209 %attr(755,root,root) %{_bindir}/coqnative
 210 %attr(755,root,root) %{_bindir}/coqpp
 211 %attr(755,root,root) %{_bindir}/coqproofworker.opt
 212 %attr(755,root,root) %{_bindir}/coqqueryworker.opt
 213 %attr(755,root,root) %{_bindir}/coqtacticworker.opt
 214 %attr(755,root,root) %{_bindir}/coqtop
 215 %attr(755,root,root) %{_bindir}/coqtop.byte
 216 %attr(755,root,root) %{_bindir}/coqtop.opt
 217 %attr(755,root,root) %{_bindir}/coqwc
 218 %attr(755,root,root) %{_bindir}/coqworkmgr
 219 %attr(755,root,root) %{_bindir}/csdpcert
 220 %attr(755,root,root) %{_bindir}/ocamllibdep
 221 %attr(755,root,root) %{_bindir}/votour
 222 %dir %{_libdir}/coq
 223 %{_libdir}/coq/theories
 224 %{_libdir}/coq/user-contrib
 225 %{_mandir}/man1/coq_makefile.1*
 226 %{_mandir}/man1/coq-tex.1*
 227 %{_mandir}/man1/coqc.1*
 228 %{_mandir}/man1/coqchk.1*
 229 %{_mandir}/man1/coqdep.1*
 230 %{_mandir}/man1/coqdoc.1*
 231 %{_mandir}/man1/coqide.1*
 232 %{_mandir}/man1/coqnative.1*
 233 %{_mandir}/man1/coqtop.1*
 234 %{_mandir}/man1/coqtop.byte.1*
 235 %{?with_ocaml_opt:%{_mandir}/man1/coqtop.opt.1*}
 236 %{_mandir}/man1/coqwc.1*
 237 %{_desktopdir}/coqide.desktop
 238 %{_pixmapsdir}/coqide.xpm
 239 %{_datadir}/%{name}
 240
 241 %files -n ocaml-coq
 242 %defattr(644,root,root,755)
 243 %dir %{_libdir}/ocaml/coq-core
 244 %{_libdir}/ocaml/coq-core/META
 245 %{_libdir}/ocaml/coq-core/revision
 246 %dir %{_libdir}/ocaml/coq-core/boot
 247 %{_libdir}/ocaml/coq-core/boot/*.cma
 248 %dir %{_libdir}/ocaml/coq-core/clib
 249 %{_libdir}/ocaml/coq-core/clib/*.cma
 250 %dir %{_libdir}/ocaml/coq-core/config
 251 %{_libdir}/ocaml/coq-core/config/*.cma
 252 %dir %{_libdir}/ocaml/coq-core/engine
 253 %{_libdir}/ocaml/coq-core/engine/*.cma
 254 %dir %{_libdir}/ocaml/coq-core/gramlib
 255 %{_libdir}/ocaml/coq-core/gramlib/*.cma
 256 %dir %{_libdir}/ocaml/coq-core/interp
 257 %{_libdir}/ocaml/coq-core/interp/*.cma
 258 %dir %{_libdir}/ocaml/coq-core/kernel
 259 %{_libdir}/ocaml/coq-core/kernel/*.cma
 260 %dir %{_libdir}/ocaml/coq-core/lib
 261 %{_libdir}/ocaml/coq-core/lib/*.cma
 262 %dir %{_libdir}/ocaml/coq-core/library
 263 %{_libdir}/ocaml/coq-core/library/*.cma
 264 %dir %{_libdir}/ocaml/coq-core/parsing
 265 %{_libdir}/ocaml/coq-core/parsing/*.cma
 266 %dir %{_libdir}/ocaml/coq-core/plugins
 267 %dir %{_libdir}/ocaml/coq-core/plugins/btauto
 268 %{_libdir}/ocaml/coq-core/plugins/btauto/*.cma
 269 %dir %{_libdir}/ocaml/coq-core/plugins/cc
 270 %{_libdir}/ocaml/coq-core/plugins/cc/*.cma
 271 %dir %{_libdir}/ocaml/coq-core/plugins/derive
 272 %{_libdir}/ocaml/coq-core/plugins/derive/*.cma
 273 %dir %{_libdir}/ocaml/coq-core/plugins/extraction
 274 %{_libdir}/ocaml/coq-core/plugins/extraction/*.cma
 275 %dir %{_libdir}/ocaml/coq-core/plugins/firstorder
 276 %{_libdir}/ocaml/coq-core/plugins/firstorder/*.cma
 277 %dir %{_libdir}/ocaml/coq-core/plugins/funind
 278 %{_libdir}/ocaml/coq-core/plugins/funind/*.cma
 279 %dir %{_libdir}/ocaml/coq-core/plugins/ltac
 280 %{_libdir}/ocaml/coq-core/plugins/ltac/*.cma
 281 %dir %{_libdir}/ocaml/coq-core/plugins/ltac2
 282 %{_libdir}/ocaml/coq-core/plugins/ltac2/*.cma
 283 %dir %{_libdir}/ocaml/coq-core/plugins/micromega
 284 %{_libdir}/ocaml/coq-core/plugins/micromega/*.cma
 285 %dir %{_libdir}/ocaml/coq-core/plugins/nsatz
 286 %{_libdir}/ocaml/coq-core/plugins/nsatz/*.cma
 287 %dir %{_libdir}/ocaml/coq-core/plugins/number_string_notation
 288 %{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.cma
 289 %dir %{_libdir}/ocaml/coq-core/plugins/ring
 290 %{_libdir}/ocaml/coq-core/plugins/ring/*.cma
 291 %dir %{_libdir}/ocaml/coq-core/plugins/rtauto
 292 %{_libdir}/ocaml/coq-core/plugins/rtauto/*.cma
 293 %dir %{_libdir}/ocaml/coq-core/plugins/ssreflect
 294 %{_libdir}/ocaml/coq-core/plugins/ssreflect/*.cma
 295 %dir %{_libdir}/ocaml/coq-core/plugins/ssrmatching
 296 %{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.cma
 297 %dir %{_libdir}/ocaml/coq-core/plugins/tauto
 298 %{_libdir}/ocaml/coq-core/plugins/tauto/*.cma
 299 %dir %{_libdir}/ocaml/coq-core/plugins/tutorial
 300 %dir %{_libdir}/ocaml/coq-core/plugins/tutorial/p0
 301 %{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.cma
 302 %dir %{_libdir}/ocaml/coq-core/plugins/tutorial/p1
 303 %{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.cma
 304 %dir %{_libdir}/ocaml/coq-core/plugins/tutorial/p2
 305 %{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.cma
 306 %dir %{_libdir}/ocaml/coq-core/plugins/tutorial/p3
 307 %{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.cma
 308 %dir %{_libdir}/ocaml/coq-core/plugins/zify
 309 %{_libdir}/ocaml/coq-core/plugins/zify/*.cma
 310 %dir %{_libdir}/ocaml/coq-core/pretyping
 311 %{_libdir}/ocaml/coq-core/pretyping/*.cma
 312 %dir %{_libdir}/ocaml/coq-core/printing
 313 %{_libdir}/ocaml/coq-core/printing/*.cma
 314 %dir %{_libdir}/ocaml/coq-core/proofs
 315 %{_libdir}/ocaml/coq-core/proofs/*.cma
 316 %dir %{_libdir}/ocaml/coq-core/stm
 317 %{_libdir}/ocaml/coq-core/stm/*.cma
 318 %dir %{_libdir}/ocaml/coq-core/sysinit
 319 %{_libdir}/ocaml/coq-core/sysinit/*.cma
 320 %dir %{_libdir}/ocaml/coq-core/tactics
 321 %{_libdir}/ocaml/coq-core/tactics/*.cma
 322 %dir %{_libdir}/ocaml/coq-core/top_printers
 323 %{_libdir}/ocaml/coq-core/top_printers/*.cma
 324 %dir %{_libdir}/ocaml/coq-core/toplevel
 325 %{_libdir}/ocaml/coq-core/toplevel/*.cma
 326 %dir %{_libdir}/ocaml/coq-core/vernac
 327 %{_libdir}/ocaml/coq-core/vernac/*.cma
 328 %dir %{_libdir}/ocaml/coq-core/vm
 329 %{_libdir}/ocaml/coq-core/vm/*.cma
 330 %dir %{_libdir}/ocaml/coqide
 331 %{_libdir}/ocaml/coqide/META
 332 %dir %{_libdir}/ocaml/coqide-server
 333 %{_libdir}/ocaml/coqide-server/META
 334 %dir %{_libdir}/ocaml/coqide-server/core
 335 %{_libdir}/ocaml/coqide-server/core/*.cma
 336 %dir %{_libdir}/ocaml/coqide-server/protocol
 337 %{_libdir}/ocaml/coqide-server/protocol/*.cma
 338 %if %{with ocaml_opt}
 339 %attr(755,root,root) %{_libdir}/ocaml/coq-core/boot/*.cmxs
 340 %attr(755,root,root) %{_libdir}/ocaml/coq-core/clib/*.cmxs
 341 %attr(755,root,root) %{_libdir}/ocaml/coq-core/config/*.cmxs
 342 %attr(755,root,root) %{_libdir}/ocaml/coq-core/engine/*.cmxs
 343 %attr(755,root,root) %{_libdir}/ocaml/coq-core/gramlib/*.cmxs
 344 %attr(755,root,root) %{_libdir}/ocaml/coq-core/interp/*.cmxs
 345 %attr(755,root,root) %{_libdir}/ocaml/coq-core/kernel/*.cmxs
 346 %attr(755,root,root) %{_libdir}/ocaml/coq-core/lib/*.cmxs
 347 %attr(755,root,root) %{_libdir}/ocaml/coq-core/library/*.cmxs
 348 %attr(755,root,root) %{_libdir}/ocaml/coq-core/parsing/*.cmxs
 349 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/btauto/*.cmxs
 350 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/cc/*.cmxs
 351 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/derive/*.cmxs
 352 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/extraction/*.cmxs
 353 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/firstorder/*.cmxs
 354 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/funind/*.cmxs
 355 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/ltac/*.cmxs
 356 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/ltac2/*.cmxs
 357 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/micromega/*.cmxs
 358 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/nsatz/*.cmxs
 359 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.cmxs
 360 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/ring/*.cmxs
 361 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/rtauto/*.cmxs
 362 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/ssreflect/*.cmxs
 363 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.cmxs
 364 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/tauto/*.cmxs
 365 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.cmxs
 366 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.cmxs
 367 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.cmxs
 368 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.cmxs
 369 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/zify/*.cmxs
 370 %attr(755,root,root) %{_libdir}/ocaml/coq-core/pretyping/*.cmxs
 371 %attr(755,root,root) %{_libdir}/ocaml/coq-core/printing/*.cmxs
 372 %attr(755,root,root) %{_libdir}/ocaml/coq-core/proofs/*.cmxs
 373 %attr(755,root,root) %{_libdir}/ocaml/coq-core/stm/*.cmxs
 374 %attr(755,root,root) %{_libdir}/ocaml/coq-core/sysinit/*.cmxs
 375 %attr(755,root,root) %{_libdir}/ocaml/coq-core/tactics/*.cmxs
 376 %attr(755,root,root) %{_libdir}/ocaml/coq-core/top_printers/*.cmxs
 377 %attr(755,root,root) %{_libdir}/ocaml/coq-core/toplevel/*.cmxs
 378 %attr(755,root,root) %{_libdir}/ocaml/coq-core/vernac/*.cmxs
 379 %attr(755,root,root) %{_libdir}/ocaml/coq-core/vm/*.cmxs
 380 %attr(755,root,root) %{_libdir}/ocaml/coqide-server/core/*.cmxs
 381 %attr(755,root,root) %{_libdir}/ocaml/coqide-server/protocol/*.cmxs
 382 %endif
 383 %attr(755,root,root) %{_libdir}/ocaml/stublibs/dllcoqrun_stubs.so
 384
 385 %files -n ocaml-coq-devel
 386 %defattr(644,root,root,755)
 387 %{_libdir}/ocaml/coq-core/dune-package
 388 %{_libdir}/ocaml/coq-core/opam
 389 %{_libdir}/ocaml/coq-core/boot/*.cmi
 390 %{_libdir}/ocaml/coq-core/boot/*.cmt
 391 %{_libdir}/ocaml/coq-core/boot/*.cmti
 392 %{_libdir}/ocaml/coq-core/boot/*.mli
 393 %{_libdir}/ocaml/coq-core/clib/*.cmi
 394 %{_libdir}/ocaml/coq-core/clib/*.cmt
 395 %{_libdir}/ocaml/coq-core/clib/*.cmti
 396 %{_libdir}/ocaml/coq-core/clib/*.mli
 397 %{_libdir}/ocaml/coq-core/config/*.cmi
 398 %{_libdir}/ocaml/coq-core/config/*.cmt
 399 %{_libdir}/ocaml/coq-core/config/*.cmti
 400 %{_libdir}/ocaml/coq-core/config/*.mli
 401 %{_libdir}/ocaml/coq-core/engine/*.cmi
 402 %{_libdir}/ocaml/coq-core/engine/*.cmt
 403 %{_libdir}/ocaml/coq-core/engine/*.cmti
 404 %{_libdir}/ocaml/coq-core/engine/*.mli
 405 %{_libdir}/ocaml/coq-core/gramlib/*.cmi
 406 %{_libdir}/ocaml/coq-core/gramlib/*.cmt
 407 %{_libdir}/ocaml/coq-core/gramlib/*.cmti
 408 %{_libdir}/ocaml/coq-core/gramlib/*.mli
 409 %{_libdir}/ocaml/coq-core/interp/*.cmi
 410 %{_libdir}/ocaml/coq-core/interp/*.cmt
 411 %{_libdir}/ocaml/coq-core/interp/*.cmti
 412 %{_libdir}/ocaml/coq-core/interp/*.mli
 413 %{_libdir}/ocaml/coq-core/kernel/*.cmi
 414 %{_libdir}/ocaml/coq-core/kernel/*.cmt
 415 %{_libdir}/ocaml/coq-core/kernel/*.cmti
 416 %{_libdir}/ocaml/coq-core/kernel/*.mli
 417 %{_libdir}/ocaml/coq-core/lib/*.cmi
 418 %{_libdir}/ocaml/coq-core/lib/*.cmt
 419 %{_libdir}/ocaml/coq-core/lib/*.cmti
 420 %{_libdir}/ocaml/coq-core/lib/*.mli
 421 %{_libdir}/ocaml/coq-core/library/*.cmi
 422 %{_libdir}/ocaml/coq-core/library/*.cmt
 423 %{_libdir}/ocaml/coq-core/library/*.cmti
 424 %{_libdir}/ocaml/coq-core/library/*.mli
 425 %{_libdir}/ocaml/coq-core/parsing/*.cmi
 426 %{_libdir}/ocaml/coq-core/parsing/*.cmt
 427 %{_libdir}/ocaml/coq-core/parsing/*.cmti
 428 %{_libdir}/ocaml/coq-core/parsing/*.mli
 429 %{_libdir}/ocaml/coq-core/plugins/btauto/*.cmi
 430 %{_libdir}/ocaml/coq-core/plugins/btauto/*.cmt
 431 %{_libdir}/ocaml/coq-core/plugins/btauto/*.cmti
 432 %{_libdir}/ocaml/coq-core/plugins/btauto/*.mli
 433 %{_libdir}/ocaml/coq-core/plugins/cc/*.cmi
 434 %{_libdir}/ocaml/coq-core/plugins/cc/*.cmt
 435 %{_libdir}/ocaml/coq-core/plugins/cc/*.cmti
 436 %{_libdir}/ocaml/coq-core/plugins/cc/*.mli
 437 %{_libdir}/ocaml/coq-core/plugins/derive/*.cmi
 438 %{_libdir}/ocaml/coq-core/plugins/derive/*.cmt
 439 %{_libdir}/ocaml/coq-core/plugins/derive/*.cmti
 440 %{_libdir}/ocaml/coq-core/plugins/derive/*.mli
 441 %{_libdir}/ocaml/coq-core/plugins/extraction/*.cmi
 442 %{_libdir}/ocaml/coq-core/plugins/extraction/*.cmt
 443 %{_libdir}/ocaml/coq-core/plugins/extraction/*.cmti
 444 %{_libdir}/ocaml/coq-core/plugins/extraction/*.mli
 445 %{_libdir}/ocaml/coq-core/plugins/firstorder/*.cmi
 446 %{_libdir}/ocaml/coq-core/plugins/firstorder/*.cmt
 447 %{_libdir}/ocaml/coq-core/plugins/firstorder/*.cmti
 448 %{_libdir}/ocaml/coq-core/plugins/firstorder/*.mli
 449 %{_libdir}/ocaml/coq-core/plugins/funind/*.cmi
 450 %{_libdir}/ocaml/coq-core/plugins/funind/*.cmt
 451 %{_libdir}/ocaml/coq-core/plugins/funind/*.cmti
 452 %{_libdir}/ocaml/coq-core/plugins/funind/*.mli
 453 %{_libdir}/ocaml/coq-core/plugins/ltac/*.cmi
 454 %{_libdir}/ocaml/coq-core/plugins/ltac/*.cmt
 455 %{_libdir}/ocaml/coq-core/plugins/ltac/*.cmti
 456 %{_libdir}/ocaml/coq-core/plugins/ltac/*.mli
 457 %{_libdir}/ocaml/coq-core/plugins/ltac2/*.cmi
 458 %{_libdir}/ocaml/coq-core/plugins/ltac2/*.cmt
 459 %{_libdir}/ocaml/coq-core/plugins/ltac2/*.cmti
 460 %{_libdir}/ocaml/coq-core/plugins/ltac2/*.mli
 461 %{_libdir}/ocaml/coq-core/plugins/micromega/*.cmi
 462 %{_libdir}/ocaml/coq-core/plugins/micromega/*.cmt
 463 %{_libdir}/ocaml/coq-core/plugins/micromega/*.cmti
 464 %{_libdir}/ocaml/coq-core/plugins/micromega/*.mli
 465 %{_libdir}/ocaml/coq-core/plugins/nsatz/*.cmi
 466 %{_libdir}/ocaml/coq-core/plugins/nsatz/*.cmt
 467 %{_libdir}/ocaml/coq-core/plugins/nsatz/*.cmti
 468 %{_libdir}/ocaml/coq-core/plugins/nsatz/*.mli
 469 %{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.cmi
 470 %{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.cmt
 471 %{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.cmti
 472 %{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.mli
 473 %{_libdir}/ocaml/coq-core/plugins/ring/*.cmi
 474 %{_libdir}/ocaml/coq-core/plugins/ring/*.cmt
 475 %{_libdir}/ocaml/coq-core/plugins/ring/*.cmti
 476 %{_libdir}/ocaml/coq-core/plugins/ring/*.mli
 477 %{_libdir}/ocaml/coq-core/plugins/rtauto/*.cmi
 478 %{_libdir}/ocaml/coq-core/plugins/rtauto/*.cmt
 479 %{_libdir}/ocaml/coq-core/plugins/rtauto/*.cmti
 480 %{_libdir}/ocaml/coq-core/plugins/rtauto/*.mli
 481 %{_libdir}/ocaml/coq-core/plugins/ssreflect/*.cmi
 482 %{_libdir}/ocaml/coq-core/plugins/ssreflect/*.cmt
 483 %{_libdir}/ocaml/coq-core/plugins/ssreflect/*.cmti
 484 %{_libdir}/ocaml/coq-core/plugins/ssreflect/*.mli
 485 %{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.cmi
 486 %{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.cmt
 487 %{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.cmti
 488 %{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.mli
 489 %{_libdir}/ocaml/coq-core/plugins/tauto/*.cmi
 490 %{_libdir}/ocaml/coq-core/plugins/tauto/*.cmt
 491 %{_libdir}/ocaml/coq-core/plugins/tauto/*.cmti
 492 %{_libdir}/ocaml/coq-core/plugins/tauto/*.mli
 493 %{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.cmi
 494 %{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.cmt
 495 %{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.cmti
 496 %{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.mli
 497 %{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.cmi
 498 %{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.cmt
 499 %{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.cmti
 500 %{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.mli
 501 %{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.cmi
 502 %{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.cmt
 503 %{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.cmti
 504 %{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.mli
 505 %{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.cmi
 506 %{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.cmt
 507 %{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.cmti
 508 %{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.mli
 509 %{_libdir}/ocaml/coq-core/plugins/zify/*.cmi
 510 %{_libdir}/ocaml/coq-core/plugins/zify/*.cmt
 511 %{_libdir}/ocaml/coq-core/plugins/zify/*.cmti
 512 %{_libdir}/ocaml/coq-core/plugins/zify/*.mli
 513 %{_libdir}/ocaml/coq-core/pretyping/*.cmi
 514 %{_libdir}/ocaml/coq-core/pretyping/*.cmt
 515 %{_libdir}/ocaml/coq-core/pretyping/*.cmti
 516 %{_libdir}/ocaml/coq-core/pretyping/*.mli
 517 %{_libdir}/ocaml/coq-core/printing/*.cmi
 518 %{_libdir}/ocaml/coq-core/printing/*.cmt
 519 %{_libdir}/ocaml/coq-core/printing/*.cmti
 520 %{_libdir}/ocaml/coq-core/printing/*.mli
 521 %{_libdir}/ocaml/coq-core/proofs/*.cmi
 522 %{_libdir}/ocaml/coq-core/proofs/*.cmt
 523 %{_libdir}/ocaml/coq-core/proofs/*.cmti
 524 %{_libdir}/ocaml/coq-core/proofs/*.mli
 525 %{_libdir}/ocaml/coq-core/stm/*.cmi
 526 %{_libdir}/ocaml/coq-core/stm/*.cmt
 527 %{_libdir}/ocaml/coq-core/stm/*.cmti
 528 %{_libdir}/ocaml/coq-core/stm/*.mli
 529 %{_libdir}/ocaml/coq-core/sysinit/*.cmi
 530 %{_libdir}/ocaml/coq-core/sysinit/*.cmt
 531 %{_libdir}/ocaml/coq-core/sysinit/*.cmti
 532 %{_libdir}/ocaml/coq-core/sysinit/*.mli
 533 %{_libdir}/ocaml/coq-core/tactics/*.cmi
 534 %{_libdir}/ocaml/coq-core/tactics/*.cmt
 535 %{_libdir}/ocaml/coq-core/tactics/*.cmti
 536 %{_libdir}/ocaml/coq-core/tactics/*.mli
 537 %{_libdir}/ocaml/coq-core/top_printers/*.cmi
 538 %{_libdir}/ocaml/coq-core/top_printers/*.cmt
 539 %{_libdir}/ocaml/coq-core/top_printers/*.cmti
 540 %{_libdir}/ocaml/coq-core/top_printers/*.mli
 541 %{_libdir}/ocaml/coq-core/toplevel/*.cmi
 542 %{_libdir}/ocaml/coq-core/toplevel/*.cmt
 543 %{_libdir}/ocaml/coq-core/toplevel/*.cmti
 544 %{_libdir}/ocaml/coq-core/toplevel/*.mli
 545 %{_libdir}/ocaml/coq-core/vernac/*.cmi
 546 %{_libdir}/ocaml/coq-core/vernac/*.cmt
 547 %{_libdir}/ocaml/coq-core/vernac/*.cmti
 548 %{_libdir}/ocaml/coq-core/vernac/*.mli
 549 %{_libdir}/ocaml/coq-core/vm/libcoqrun_stubs.a
 550 %{_libdir}/ocaml/coq-core/vm/*.cmi
 551 %{_libdir}/ocaml/coq-core/vm/*.cmt
 552 %{_libdir}/ocaml/coqide/dune-package
 553 %{_libdir}/ocaml/coqide/opam
 554 %{_libdir}/ocaml/coqide-server/dune-package
 555 %{_libdir}/ocaml/coqide-server/opam
 556 %{_libdir}/ocaml/coqide-server/core/*.cmi
 557 %{_libdir}/ocaml/coqide-server/core/*.cmt
 558 %{_libdir}/ocaml/coqide-server/core/*.cmti
 559 %{_libdir}/ocaml/coqide-server/core/*.mli
 560 %{_libdir}/ocaml/coqide-server/protocol/*.cmi
 561 %{_libdir}/ocaml/coqide-server/protocol/*.cmt
 562 %{_libdir}/ocaml/coqide-server/protocol/*.cmti
 563 %{_libdir}/ocaml/coqide-server/protocol/*.mli
 564 %if %{with ocaml_opt}
 565 %{_libdir}/ocaml/coq-core/boot/boot.a
 566 %{_libdir}/ocaml/coq-core/boot/*.cmx
 567 %{_libdir}/ocaml/coq-core/boot/*.cmxa
 568 %{_libdir}/ocaml/coq-core/clib/clib.a
 569 %{_libdir}/ocaml/coq-core/clib/*.cmx
 570 %{_libdir}/ocaml/coq-core/clib/*.cmxa
 571 %{_libdir}/ocaml/coq-core/config/config.a
 572 %{_libdir}/ocaml/coq-core/config/*.cmx
 573 %{_libdir}/ocaml/coq-core/config/*.cmxa
 574 %{_libdir}/ocaml/coq-core/engine/engine.a
 575 %{_libdir}/ocaml/coq-core/engine/*.cmx
 576 %{_libdir}/ocaml/coq-core/engine/*.cmxa
 577 %{_libdir}/ocaml/coq-core/gramlib/gramlib.a
 578 %{_libdir}/ocaml/coq-core/gramlib/*.cmx
 579 %{_libdir}/ocaml/coq-core/gramlib/*.cmxa
 580 %{_libdir}/ocaml/coq-core/interp/interp.a
 581 %{_libdir}/ocaml/coq-core/interp/*.cmx
 582 %{_libdir}/ocaml/coq-core/interp/*.cmxa
 583 %{_libdir}/ocaml/coq-core/kernel/kernel.a
 584 %{_libdir}/ocaml/coq-core/kernel/*.cmx
 585 %{_libdir}/ocaml/coq-core/kernel/*.cmxa
 586 %{_libdir}/ocaml/coq-core/lib/lib.a
 587 %{_libdir}/ocaml/coq-core/lib/*.cmx
 588 %{_libdir}/ocaml/coq-core/lib/*.cmxa
 589 %{_libdir}/ocaml/coq-core/library/library.a
 590 %{_libdir}/ocaml/coq-core/library/*.cmx
 591 %{_libdir}/ocaml/coq-core/library/*.cmxa
 592 %{_libdir}/ocaml/coq-core/parsing/parsing.a
 593 %{_libdir}/ocaml/coq-core/parsing/*.cmx
 594 %{_libdir}/ocaml/coq-core/parsing/*.cmxa
 595 %{_libdir}/ocaml/coq-core/plugins/btauto/btauto_plugin.a
 596 %{_libdir}/ocaml/coq-core/plugins/btauto/*.cmx
 597 %{_libdir}/ocaml/coq-core/plugins/btauto/*.cmxa
 598 %{_libdir}/ocaml/coq-core/plugins/cc/cc_plugin.a
 599 %{_libdir}/ocaml/coq-core/plugins/cc/*.cmx
 600 %{_libdir}/ocaml/coq-core/plugins/cc/*.cmxa
 601 %{_libdir}/ocaml/coq-core/plugins/derive/derive_plugin.a
 602 %{_libdir}/ocaml/coq-core/plugins/derive/*.cmx
 603 %{_libdir}/ocaml/coq-core/plugins/derive/*.cmxa
 604 %{_libdir}/ocaml/coq-core/plugins/extraction/extraction_plugin.a
 605 %{_libdir}/ocaml/coq-core/plugins/extraction/*.cmx
 606 %{_libdir}/ocaml/coq-core/plugins/extraction/*.cmxa
 607 %{_libdir}/ocaml/coq-core/plugins/firstorder/firstorder_plugin.a
 608 %{_libdir}/ocaml/coq-core/plugins/firstorder/*.cmx
 609 %{_libdir}/ocaml/coq-core/plugins/firstorder/*.cmxa
 610 %{_libdir}/ocaml/coq-core/plugins/funind/funind_plugin.a
 611 %{_libdir}/ocaml/coq-core/plugins/funind/*.cmx
 612 %{_libdir}/ocaml/coq-core/plugins/funind/*.cmxa
 613 %{_libdir}/ocaml/coq-core/plugins/ltac/ltac_plugin.a
 614 %{_libdir}/ocaml/coq-core/plugins/ltac/*.cmx
 615 %{_libdir}/ocaml/coq-core/plugins/ltac/*.cmxa
 616 %{_libdir}/ocaml/coq-core/plugins/ltac2/ltac2_plugin.a
 617 %{_libdir}/ocaml/coq-core/plugins/ltac2/*.cmx
 618 %{_libdir}/ocaml/coq-core/plugins/ltac2/*.cmxa
 619 %{_libdir}/ocaml/coq-core/plugins/micromega/micromega_plugin.a
 620 %{_libdir}/ocaml/coq-core/plugins/micromega/*.cmx
 621 %{_libdir}/ocaml/coq-core/plugins/micromega/*.cmxa
 622 %{_libdir}/ocaml/coq-core/plugins/nsatz/nsatz_plugin.a
 623 %{_libdir}/ocaml/coq-core/plugins/nsatz/*.cmx
 624 %{_libdir}/ocaml/coq-core/plugins/nsatz/*.cmxa
 625 %{_libdir}/ocaml/coq-core/plugins/number_string_notation/number_string_notation_plugin.a
 626 %{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.cmx
 627 %{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.cmxa
 628 %{_libdir}/ocaml/coq-core/plugins/ring/ring_plugin.a
 629 %{_libdir}/ocaml/coq-core/plugins/ring/*.cmx
 630 %{_libdir}/ocaml/coq-core/plugins/ring/*.cmxa
 631 %{_libdir}/ocaml/coq-core/plugins/rtauto/rtauto_plugin.a
 632 %{_libdir}/ocaml/coq-core/plugins/rtauto/*.cmx
 633 %{_libdir}/ocaml/coq-core/plugins/rtauto/*.cmxa
 634 %{_libdir}/ocaml/coq-core/plugins/ssreflect/ssreflect_plugin.a
 635 %{_libdir}/ocaml/coq-core/plugins/ssreflect/*.cmx
 636 %{_libdir}/ocaml/coq-core/plugins/ssreflect/*.cmxa
 637 %{_libdir}/ocaml/coq-core/plugins/ssrmatching/ssrmatching_plugin.a
 638 %{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.cmx
 639 %{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.cmxa
 640 %{_libdir}/ocaml/coq-core/plugins/tauto/tauto_plugin.a
 641 %{_libdir}/ocaml/coq-core/plugins/tauto/*.cmx
 642 %{_libdir}/ocaml/coq-core/plugins/tauto/*.cmxa
 643 %{_libdir}/ocaml/coq-core/plugins/tutorial/p0/tuto0_plugin.a
 644 %{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.cmx
 645 %{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.cmxa
 646 %{_libdir}/ocaml/coq-core/plugins/tutorial/p1/tuto1_plugin.a
 647 %{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.cmx
 648 %{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.cmxa
 649 %{_libdir}/ocaml/coq-core/plugins/tutorial/p2/tuto2_plugin.a
 650 %{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.cmx
 651 %{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.cmxa
 652 %{_libdir}/ocaml/coq-core/plugins/tutorial/p3/tuto3_plugin.a
 653 %{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.cmx
 654 %{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.cmxa
 655 %{_libdir}/ocaml/coq-core/plugins/zify/zify_plugin.a
 656 %{_libdir}/ocaml/coq-core/plugins/zify/*.cmx
 657 %{_libdir}/ocaml/coq-core/plugins/zify/*.cmxa
 658 %{_libdir}/ocaml/coq-core/pretyping/pretyping.a
 659 %{_libdir}/ocaml/coq-core/pretyping/*.cmx
 660 %{_libdir}/ocaml/coq-core/pretyping/*.cmxa
 661 %{_libdir}/ocaml/coq-core/printing/printing.a
 662 %{_libdir}/ocaml/coq-core/printing/*.cmx
 663 %{_libdir}/ocaml/coq-core/printing/*.cmxa
 664 %{_libdir}/ocaml/coq-core/proofs/proofs.a
 665 %{_libdir}/ocaml/coq-core/proofs/*.cmx
 666 %{_libdir}/ocaml/coq-core/proofs/*.cmxa
 667 %{_libdir}/ocaml/coq-core/stm/stm.a
 668 %{_libdir}/ocaml/coq-core/stm/*.cmx
 669 %{_libdir}/ocaml/coq-core/stm/*.cmxa
 670 %{_libdir}/ocaml/coq-core/sysinit/sysinit.a
 671 %{_libdir}/ocaml/coq-core/sysinit/*.cmx
 672 %{_libdir}/ocaml/coq-core/sysinit/*.cmxa
 673 %{_libdir}/ocaml/coq-core/tactics/tactics.a
 674 %{_libdir}/ocaml/coq-core/tactics/*.cmx
 675 %{_libdir}/ocaml/coq-core/tactics/*.cmxa
 676 %{_libdir}/ocaml/coq-core/top_printers/top_printers.a
 677 %{_libdir}/ocaml/coq-core/top_printers/*.cmx
 678 %{_libdir}/ocaml/coq-core/top_printers/*.cmxa
 679 %{_libdir}/ocaml/coq-core/toplevel/toplevel.a
 680 %{_libdir}/ocaml/coq-core/toplevel/*.cmx
 681 %{_libdir}/ocaml/coq-core/toplevel/*.cmxa
 682 %{_libdir}/ocaml/coq-core/vernac/vernac.a
 683 %{_libdir}/ocaml/coq-core/vernac/*.cmx
 684 %{_libdir}/ocaml/coq-core/vernac/*.cmxa
 685 %{_libdir}/ocaml/coq-core/vm/coqrun.a
 686 %{_libdir}/ocaml/coq-core/vm/*.cmx
 687 %{_libdir}/ocaml/coq-core/vm/*.cmxa
 688 %{_libdir}/ocaml/coqide-server/core/core.a
 689 %{_libdir}/ocaml/coqide-server/core/*.cmx
 690 %{_libdir}/ocaml/coqide-server/core/*.cmxa
 691 %{_libdir}/ocaml/coqide-server/protocol/protocol.a
 692 %{_libdir}/ocaml/coqide-server/protocol/*.cmx
 693 %{_libdir}/ocaml/coqide-server/protocol/*.cmxa
 694 %endif
 695
 696 %files latex
 697 %defattr(644,root,root,755)
 698 %{_datadir}/texmf/tex/latex/misc/coqdoc.sty