This result is black-listed as it is considered as too hard to reproduce / to solve. If you find a way to fix this package, please make a pull-request to github.com/coq/opam-coq-archive. The list of black-listed packages is in black_list.rb.
# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-num base Num library distributed with the OCaml compiler
base-ocamlbuild base OCamlbuild binary and libraries distributed with the OCaml compiler
base-threads base
base-unix base
camlp5 7.14 Preprocessor-pretty-printer of OCaml
conf-findutils 1 Virtual package relying on findutils
conf-perl 2 Virtual package relying on perl
coq 8.4.5 Formal proof management system.
num 0 The Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.02.3 The OCaml compiler (virtual package)
ocaml-base-compiler 4.02.3 Official 4.02.3 release
ocaml-config 1 OCaml Switch Configuration
ocamlbuild 0 Build system distributed with the OCaml compiler since OCaml 3.10.0
# opam file:
opam-version: "2.0"
maintainer: "Reynald Affeldt <reynald.affeldt@aist.go.jp>"
homepage: "https://github.com/math-comp/analysis"
dev-repo: "git+https://github.com/math-comp/analysis.git"
bug-reports: "https://github.com/math-comp/analysis/issues"
license: "CECILL-C"
synopsis: "A library for classical logic for mathematical components"
description: """
This repository contains a library for classical logic for
the Coq proof-assistant and using the Mathematical Components library."""
build: [make "-C" "classical" "-j%{jobs}%"]
install: [make "-C" "classical" "install"]
depends: [
"coq" { (>= "8.14" & < "8.18~") | (= "dev") }
"coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.17~") | (= "dev") }
"coq-mathcomp-fingroup"
"coq-mathcomp-algebra"
"coq-mathcomp-finmap" { (>= "1.5.1" & < "1.6~") | (= "dev") }
"coq-hierarchy-builder" { (>= "1.2.0") }
]
tags: [
"category:Mathematics/Logic/Classical logic"
"keyword:classical logic"
"keyword:sets"
"date:2023-02-24"
"logpath:mathcomp.classical"
]
authors: [
"Reynald Affeldt"
"Yves Bertot"
"Cyril Cohen"
"Marie Kerjean"
"Assia Mahboubi"
"Damien Rouhling"
"Pierre Roux"
"Kazuhiko Sakaguchi"
"Zachary Stone"
"Pierre-Yves Strub"
"Laurent Théry"
]
url {
src: "https://github.com/math-comp/analysis/archive/0.6.1.tar.gz"
checksum: "sha512=0837e94be865437baba6387c25d14cb699bd80c680f619cbccb144982c1b256e1ace6cce7c430a5db4a25ce86463a7715f967133bbc243b6cd21c3a607368784"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-mathcomp-classical.0.6.1 coq.8.4.5[NOTE] Package coq is already installed (current version is 8.4.5).
The following dependencies couldn't be met:
- coq-mathcomp-classical -> coq >= dev -> ocaml >= 4.05.0
base of this switch (use `--unlock-base' to force)
- coq-mathcomp-classical -> coq >= dev -> coq-core -> ocaml >= 4.09.0
base of this switch (use `--unlock-base' to force)
No solution found, exiting
Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
opam remove -y coq; opam install -y --show-action --unlock-base coq-mathcomp-classical.0.6.1The following actions will be performed:
- remove coq 8.4.5
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[WARNING] While removing coq.8.4.5: not removing files that changed since:
- share/emacs/site-lisp/coqdoc.sty
- share/emacs/site-lisp/coq.el
- share/emacs/site-lisp/coq-syntax.el
- share/emacs/site-lisp/coq-inferior.el
- share/emacs/site-lisp/coq-font-lock.el
- share/emacs/site-lisp/coq-db.el
- share/coq/coq.png
- man/man1/gallina.1
- man/man1/coqwc.1
- man/man1/coqtop.opt.1
- man/man1/coqtop.byte.1
- man/man1/coqtop.1
- man/man1/coqmktop.1
- man/man1/coqide.1
- man/man1/coqdoc.1
- man/man1/coqdep.1
- man/man1/coqchk.1
- man/man1/coqc.1
- man/man1/coq_makefile.1
- man/man1/coq-tex.1
- lib/coq/toplevel/whelp.cmi
- lib/coq/toplevel/vernacinterp.cmi
- lib/coq/toplevel/vernacexpr.cmi
- lib/coq/toplevel/vernacentries.cmi
- lib/coq/toplevel/vernac.cmi
- lib/coq/toplevel/usage.cmi
- lib/coq/toplevel/toplevel.cmxa
- lib/coq/toplevel/toplevel.cmi
- lib/coq/toplevel/toplevel.cma
- lib/coq/toplevel/toplevel.a
- lib/coq/toplevel/search.cmi
- lib/coq/toplevel/record.cmi
- lib/coq/toplevel/mltop.cmi
- lib/coq/toplevel/metasyntax.cmi
- lib/coq/toplevel/libtypes.cmi
- lib/coq/toplevel/lemmas.cmi
- lib/coq/toplevel/interface.cmi
- lib/coq/toplevel/indschemes.cmi
- lib/coq/toplevel/ind_tables.cmi
- lib/coq/toplevel/ide_slave.cmi
- lib/coq/toplevel/ide_intf.cmi
- lib/coq/toplevel/himsg.cmi
- lib/coq/toplevel/discharge.cmi
- lib/coq/toplevel/coqtop.cmi
- lib/coq/toplevel/coqinit.cmi
- lib/coq/toplevel/command.cmi
- lib/coq/toplevel/classes.cmi
- lib/coq/toplevel/class.cmi
- lib/coq/toplevel/cerrors.cmi
- lib/coq/toplevel/backtrack.cmi
- lib/coq/toplevel/autoinstance.cmi
- lib/coq/toplevel/auto_ind_decl.cmi
- lib/coq/tools/coqdoc/coqdoc.sty
- lib/coq/tools/coqdoc/coqdoc.css
- lib/coq/theories/ZArith/auxiliary.vo
- lib/coq/theories/ZArith/Zwf.vo
- lib/coq/theories/ZArith/Zsqrt_compat.vo
- lib/coq/theories/ZArith/Zquot.vo
- lib/coq/theories/ZArith/Zpower.vo
- lib/coq/theories/ZArith/Zpow_facts.vo
- lib/coq/theories/ZArith/Zpow_def.vo
- lib/coq/theories/ZArith/Zpow_alt.vo
- lib/coq/theories/ZArith/Zorder.vo
- lib/coq/theories/ZArith/Znumtheory.vo
- lib/coq/theories/ZArith/Znat.vo
- lib/coq/theories/ZArith/Zmisc.vo
- lib/coq/theories/ZArith/Zminmax.vo
- lib/coq/theories/ZArith/Zmin.vo
- lib/coq/theories/ZArith/Zmax.vo
- lib/coq/theories/ZArith/Zlogarithm.vo
- lib/coq/theories/ZArith/Zhints.vo
- lib/coq/theories/ZArith/Zgcd_alt.vo
- lib/coq/theories/ZArith/Zeven.vo
- lib/coq/theories/ZArith/Zeuclid.vo
- lib/coq/theories/ZArith/Zdiv.vo
- lib/coq/theories/ZArith/Zdigits.vo
- lib/coq/theories/ZArith/Zcomplements.vo
- lib/coq/theories/ZArith/Zcompare.vo
- lib/coq/theories/ZArith/Zbool.vo
- lib/coq/theories/ZArith/Zabs.vo
- lib/coq/theories/ZArith/ZOdiv_def.vo
- lib/coq/theories/ZArith/ZOdiv.vo
- lib/coq/theories/ZArith/ZArith_dec.vo
- lib/coq/theories/ZArith/ZArith_base.vo
- lib/coq/theories/ZArith/ZArith.vo
- lib/coq/theories/ZArith/Wf_Z.vo
- lib/coq/theories/ZArith/Int.vo
- lib/coq/theories/ZArith/BinIntDef.vo
- lib/coq/theories/ZArith/BinInt.vo
- lib/coq/theories/Wellfounded/Wellfounded.vo
- lib/coq/theories/Wellfounded/Well_Ordering.vo
- lib/coq/theories/Wellfounded/Union.vo
- lib/coq/theories/Wellfounded/Transitive_Closure.vo
- lib/coq/theories/Wellfounded/Lexicographic_Product.vo
- lib/coq/theories/Wellfounded/Lexicographic_Exponentiation.vo
- lib/coq/theories/Wellfounded/Inverse_Image.vo
- lib/coq/theories/Wellfounded/Inclusion.vo
- lib/coq/theories/Wellfounded/Disjoint_Union.vo
- lib/coq/theories/Vectors/VectorSpec.vo
- lib/coq/theories/Vectors/VectorDef.vo
- lib/coq/theories/Vectors/Vector.vo
- lib/coq/theories/Vectors/Fin.vo
- lib/coq/theories/Unicode/Utf8_core.vo
- lib/coq/theories/Unicode/Utf8.vo
- lib/coq/theories/Structures/OrdersTac.vo
- lib/coq/theories/Structures/OrdersLists.vo
- lib/coq/theories/Structures/OrdersFacts.vo
- lib/coq/theories/Structures/OrdersEx.vo
- lib/coq/theories/Structures/OrdersAlt.vo
- lib/coq/theories/Structures/Orders.vo
- lib/coq/theories/Structures/OrderedTypeEx.vo
- lib/coq/theories/Structures/OrderedTypeAlt.vo
- lib/coq/theories/Structures/OrderedType.vo
- lib/coq/theories/Structures/GenericMinMax.vo
- lib/coq/theories/Structures/EqualitiesFacts.vo
- lib/coq/theories/Structures/Equalities.vo
- lib/coq/theories/Structures/DecidableTypeEx.vo
- lib/coq/theories/Structures/DecidableType.vo
- lib/coq/theories/Strings/String.vo
- lib/coq/theories/Strings/Ascii.vo
- lib/coq/theories/Sorting/Sorting.vo
- lib/coq/theories/Sorting/Sorted.vo
- lib/coq/theories/Sorting/Permutation.vo
- lib/coq/theories/Sorting/PermutSetoid.vo
- lib/coq/theories/Sorting/PermutEq.vo
- lib/coq/theories/Sorting/Mergesort.vo
- lib/coq/theories/Sorting/Heap.vo
- lib/coq/theories/Sets/Uniset.vo
- lib/coq/theories/Sets/Relations_3_facts.vo
- lib/coq/theories/Sets/Relations_3.vo
- lib/coq/theories/Sets/Relations_2_facts.vo
- lib/coq/theories/Sets/Relations_2.vo
- lib/coq/theories/Sets/Relations_1_facts.vo
- lib/coq/theories/Sets/Relations_1.vo
- lib/coq/theories/Sets/Powerset_facts.vo
- lib/coq/theories/Sets/Powerset_Classical_facts.vo
- lib/coq/theories/Sets/Powerset.vo
- lib/coq/theories/Sets/Permut.vo
- lib/coq/theories/Sets/Partial_Order.vo
- lib/coq/theories/Sets/Multiset.vo
- lib/coq/theories/Sets/Integers.vo
- lib/coq/theories/Sets/Infinite_sets.vo
- lib/coq/theories/Sets/Image.vo
- lib/coq/theories/Sets/Finite_sets_facts.vo
- lib/coq/theories/Sets/Finite_sets.vo
- lib/coq/theories/Sets/Ensembles.vo
- lib/coq/theories/Sets/Cpo.vo
- lib/coq/theories/Sets/Constructive_sets.vo
- lib/coq/theories/Sets/Classical_sets.vo
- lib/coq/theories/Setoids/Setoid.vo
- lib/coq/theories/Relations/Relations.vo
- lib/coq/theories/Relations/Relation_Operators.vo
- lib/coq/theories/Relations/Relation_Definitions.vo
- lib/coq/theories/Relations/Operators_Properties.vo
- lib/coq/theories/Reals/Sqrt_reg.vo
- lib/coq/theories/Reals/SplitRmult.vo
- lib/coq/theories/Reals/SplitAbsolu.vo
- lib/coq/theories/Reals/SeqSeries.vo
- lib/coq/theories/Reals/SeqProp.vo
- lib/coq/theories/Reals/Rtrigo_reg.vo
- lib/coq/theories/Reals/Rtrigo_fun.vo
- lib/coq/theories/Reals/Rtrigo_def.vo
- lib/coq/theories/Reals/Rtrigo_calc.vo
- lib/coq/theories/Reals/Rtrigo_alt.vo
- lib/coq/theories/Reals/Rtrigo1.vo
- lib/coq/theories/Reals/Rtrigo.vo
- lib/coq/theories/Reals/Rtopology.vo
- lib/coq/theories/Reals/Rsqrt_def.vo
- lib/coq/theories/Reals/Rsigma.vo
- lib/coq/theories/Reals/Rseries.vo
- lib/coq/theories/Reals/Rprod.vo
- lib/coq/theories/Reals/Rpower.vo
- lib/coq/theories/Reals/Rpow_def.vo
- lib/coq/theories/Reals/Rminmax.vo
- lib/coq/theories/Reals/Rlogic.vo
- lib/coq/theories/Reals/Rlimit.vo
- lib/coq/theories/Reals/RiemannInt_SF.vo
- lib/coq/theories/Reals/RiemannInt.vo
- lib/coq/theories/Reals/Rgeom.vo
- lib/coq/theories/Reals/Rfunctions.vo
- lib/coq/theories/Reals/Reals.vo
- lib/coq/theories/Reals/Rderiv.vo
- lib/coq/theories/Reals/Rdefinitions.vo
- lib/coq/theories/Reals/Rcomplete.vo
- lib/coq/theories/Reals/Rbasic_fun.vo
- lib/coq/theories/Reals/Rbase.vo
- lib/coq/theories/Reals/Raxioms.vo
- lib/coq/theories/Reals/Ratan.vo
- lib/coq/theories/Reals/Ranalysis_reg.vo
- lib/coq/theories/Reals/Ranalysis5.vo
- lib/coq/theories/Reals/Ranalysis4.vo
- lib/coq/theories/Reals/Ranalysis3.vo
- lib/coq/theories/Reals/Ranalysis2.vo
- lib/coq/theories/Reals/Ranalysis1.vo
- lib/coq/theories/Reals/Ranalysis.vo
- lib/coq/theories/Reals/R_sqrt.vo
- lib/coq/theories/Reals/R_sqr.vo
- lib/coq/theories/Reals/R_Ifp.vo
- lib/coq/theories/Reals/ROrderedType.vo
- lib/coq/theories/Reals/RList.vo
[...] truncated
t.vo
- lib/coq/plugins/extraction/ExtrOcamlIntConv.vo
- lib/coq/plugins/extraction/ExtrOcamlBigIntConv.vo
- lib/coq/plugins/extraction/ExtrOcamlBasic.vo
- lib/coq/plugins/decl_mode/ppdecl_proof.cmi
- lib/coq/plugins/decl_mode/g_decl_mode.cmi
- lib/coq/plugins/decl_mode/decl_proof_instr.cmi
- lib/coq/plugins/decl_mode/decl_mode_plugin_mod.cmi
- lib/coq/plugins/decl_mode/decl_mode_plugin.cmxs
- lib/coq/plugins/decl_mode/decl_mode_plugin.cma
- lib/coq/plugins/decl_mode/decl_mode.cmi
- lib/coq/plugins/decl_mode/decl_interp.cmi
- lib/coq/plugins/decl_mode/decl_expr.cmi
- lib/coq/plugins/cc/g_congruence.cmi
- lib/coq/plugins/cc/cctac.cmi
- lib/coq/plugins/cc/ccproof.cmi
- lib/coq/plugins/cc/ccalgo.cmi
- lib/coq/plugins/cc/cc_plugin_mod.cmi
- lib/coq/plugins/cc/cc_plugin.cmxs
- lib/coq/plugins/cc/cc_plugin.cma
- lib/coq/parsing/tok.cmi
- lib/coq/parsing/tactic_printer.cmi
- lib/coq/parsing/q_util.cmi
- lib/coq/parsing/printmod.cmi
- lib/coq/parsing/printer.cmi
- lib/coq/parsing/prettyp.cmi
- lib/coq/parsing/ppvernac.cmi
- lib/coq/parsing/pptactic.cmi
- lib/coq/parsing/ppconstr.cmi
- lib/coq/parsing/pcoq.cmi
- lib/coq/parsing/parsing.cmxa
- lib/coq/parsing/parsing.cma
- lib/coq/parsing/parsing.a
- lib/coq/parsing/lexer.cmi
- lib/coq/parsing/highparsing.cmxa
- lib/coq/parsing/highparsing.cma
- lib/coq/parsing/highparsing.a
- lib/coq/parsing/grammar.cma
- lib/coq/parsing/g_xml.cmi
- lib/coq/parsing/g_vernac.cmi
- lib/coq/parsing/g_tactic.cmi
- lib/coq/parsing/g_proofs.cmi
- lib/coq/parsing/g_prim.cmi
- lib/coq/parsing/g_ltac.cmi
- lib/coq/parsing/g_constr.cmi
- lib/coq/parsing/extrawit.cmi
- lib/coq/parsing/extend.cmi
- lib/coq/parsing/egrammar.cmi
- lib/coq/library/summary.cmi
- lib/coq/library/states.cmi
- lib/coq/library/nametab.cmi
- lib/coq/library/nameops.cmi
- lib/coq/library/library.cmxa
- lib/coq/library/library.cmi
- lib/coq/library/library.cma
- lib/coq/library/library.a
- lib/coq/library/libobject.cmi
- lib/coq/library/libnames.cmi
- lib/coq/library/lib.cmi
- lib/coq/library/impargs.cmi
- lib/coq/library/heads.cmi
- lib/coq/library/goptionstyp.cmi
- lib/coq/library/goptions.cmi
- lib/coq/library/global.cmi
- lib/coq/library/dischargedhypsmap.cmi
- lib/coq/library/decls.cmi
- lib/coq/library/declaremods.cmi
- lib/coq/library/declare.cmi
- lib/coq/library/decl_kinds.cmi
- lib/coq/library/assumptions.cmi
- lib/coq/libcoqrun.a
- lib/coq/lib/xml_utils.cmi
- lib/coq/lib/xml_parser.cmi
- lib/coq/lib/xml_lexer.cmi
- lib/coq/lib/util.cmi
- lib/coq/lib/unionfind.cmi
- lib/coq/lib/unicodetable.cmi
- lib/coq/lib/tries.cmi
- lib/coq/lib/system.cmi
- lib/coq/lib/store.cmi
- lib/coq/lib/segmenttree.cmi
- lib/coq/lib/rtree.cmi
- lib/coq/lib/profile.cmi
- lib/coq/lib/predicate.cmi
- lib/coq/lib/pp_control.cmi
- lib/coq/lib/pp.cmi
- lib/coq/lib/option.cmi
- lib/coq/lib/lib.cmxa
- lib/coq/lib/lib.cma
- lib/coq/lib/lib.a
- lib/coq/lib/heap.cmi
- lib/coq/lib/hashtbl_alt.cmi
- lib/coq/lib/hashcons.cmi
- lib/coq/lib/gmapl.cmi
- lib/coq/lib/gmap.cmi
- lib/coq/lib/fset.cmi
- lib/coq/lib/fmap.cmi
- lib/coq/lib/flags.cmi
- lib/coq/lib/explore.cmi
- lib/coq/lib/errors.cmi
- lib/coq/lib/envars.cmi
- lib/coq/lib/dyn.cmi
- lib/coq/lib/dnet.cmi
- lib/coq/lib/compat.cmi
- lib/coq/lib/bigint.cmi
- lib/coq/kernel/vm.cmi
- lib/coq/kernel/vconv.cmi
- lib/coq/kernel/univ.cmi
- lib/coq/kernel/typeops.cmi
- lib/coq/kernel/type_errors.cmi
- lib/coq/kernel/term_typing.cmi
- lib/coq/kernel/term.cmi
- lib/coq/kernel/subtyping.cmi
- lib/coq/kernel/sign.cmi
- lib/coq/kernel/safe_typing.cmi
- lib/coq/kernel/retroknowledge.cmi
- lib/coq/kernel/reduction.cmi
- lib/coq/kernel/pre_env.cmi
- lib/coq/kernel/names.cmi
- lib/coq/kernel/modops.cmi
- lib/coq/kernel/mod_typing.cmi
- lib/coq/kernel/mod_subst.cmi
- lib/coq/kernel/kernel.cmxa
- lib/coq/kernel/kernel.cma
- lib/coq/kernel/kernel.a
- lib/coq/kernel/inductive.cmi
- lib/coq/kernel/indtypes.cmi
- lib/coq/kernel/esubst.cmi
- lib/coq/kernel/environ.cmi
- lib/coq/kernel/entries.cmi
- lib/coq/kernel/declarations.cmi
- lib/coq/kernel/csymtable.cmi
- lib/coq/kernel/copcodes.cmi
- lib/coq/kernel/cooking.cmi
- lib/coq/kernel/conv_oracle.cmi
- lib/coq/kernel/closure.cmi
- lib/coq/kernel/cemitcodes.cmi
- lib/coq/kernel/cbytegen.cmi
- lib/coq/kernel/cbytecodes.cmi
- lib/coq/interp/topconstr.cmi
- lib/coq/interp/syntax_def.cmi
- lib/coq/interp/smartlocate.cmi
- lib/coq/interp/reserve.cmi
- lib/coq/interp/ppextend.cmi
- lib/coq/interp/notation.cmi
- lib/coq/interp/modintern.cmi
- lib/coq/interp/interp.cmxa
- lib/coq/interp/interp.cma
- lib/coq/interp/interp.a
- lib/coq/interp/implicit_quantifiers.cmi
- lib/coq/interp/genarg.cmi
- lib/coq/interp/dumpglob.cmi
- lib/coq/interp/coqlib.cmi
- lib/coq/interp/constrintern.cmi
- lib/coq/interp/constrextern.cmi
- lib/coq/dllcoqrun.so
- lib/coq/config/coqide-gtk2rc
- lib/coq/config/coq_config.o
- lib/coq/config/coq_config.cmx
- lib/coq/config/coq_config.cmo
- lib/coq/config/coq_config.cmi
- doc/FAQ-CoqIde
- bin/coqtop.opt
- bin/coqtop.byte
- bin/coqchk.opt
[NOTE] While removing coq.8.4.5: not removing non-empty directories:
- share/emacs/site-lisp
- share/coq
- lib/coq/toplevel
- lib/coq/tools/coqdoc
- lib/coq/theories/ZArith
- lib/coq/theories/Wellfounded
- lib/coq/theories/Vectors
- lib/coq/theories/Unicode
- lib/coq/theories/Structures
- lib/coq/theories/Strings
- lib/coq/theories/Sorting
- lib/coq/theories/Sets
- lib/coq/theories/Setoids
- lib/coq/theories/Relations
- lib/coq/theories/Reals
- lib/coq/theories/QArith
- lib/coq/theories/Program
- lib/coq/theories/PArith
- lib/coq/theories/Numbers/Rational/SpecViaQ
- lib/coq/theories/Numbers/Rational/BigQ
- lib/coq/theories/Numbers/Natural/SpecViaZ
- lib/coq/theories/Numbers/Natural/Peano
- lib/coq/theories/Numbers/Natural/Binary
- lib/coq/theories/Numbers/Natural/BigN
- lib/coq/theories/Numbers/Natural/Abstract
- lib/coq/theories/Numbers/NatInt
- lib/coq/theories/Numbers/Integer/SpecViaZ
- lib/coq/theories/Numbers/Integer/NatPairs
- lib/coq/theories/Numbers/Integer/Binary
- lib/coq/theories/Numbers/Integer/BigZ
- lib/coq/theories/Numbers/Integer/Abstract
- lib/coq/theories/Numbers/Cyclic/ZModulo
- lib/coq/theories/Numbers/Cyclic/Int31
- lib/coq/theories/Numbers/Cyclic/DoubleCyclic
- lib/coq/theories/Numbers/Cyclic/Abstract
- lib/coq/theories/NArith
- lib/coq/theories/MSets
- lib/coq/theories/Logic
- lib/coq/theories/Lists
- lib/coq/theories/Init
- lib/coq/theories/FSets
- lib/coq/theories/Classes
- lib/coq/theories/Bool
- lib/coq/theories/Arith
- lib/coq/tactics
- lib/coq/states
- lib/coq/proofs
- lib/coq/pretyping
- lib/coq/plugins/xml
- lib/coq/plugins/syntax
- lib/coq/plugins/subtac
- lib/coq/plugins/setoid_ring
- lib/coq/plugins/rtauto
- lib/coq/plugins/romega
- lib/coq/plugins/ring
- lib/coq/plugins/quote
- lib/coq/plugins/omega
- lib/coq/plugins/nsatz
- lib/coq/plugins/micromega
- lib/coq/plugins/funind
- lib/coq/plugins/fourier
- lib/coq/plugins/firstorder
- lib/coq/plugins/field
- lib/coq/plugins/extraction
- lib/coq/plugins/decl_mode
- lib/coq/plugins/cc
- lib/coq/parsing
- lib/coq/library
- lib/coq/kernel
- lib/coq/interp
- lib/coq/config
-> removed coq.8.4.5
Done.
# Run eval $(opam env) to update the current shell environment
[ERROR] Sorry, resolution of the request timed out.
Try to specify a simpler request, use a different solver, or increase the allowed time by setting OPAMSOLVERTIMEOUT to a bigger value (currently, it is set to 600.0 seconds).
The middle of the output is truncated (maximum 20000 characters)
truetrueNo files were installed.
true