(2020-09-09 03:51:12 UTC)
# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-num base Num library distributed with the OCaml compiler
base-threads base
base-unix base
camlp4 4.05+1 Camlp4 is a system for writing extensible parsers for programming languages
conf-findutils 1 Virtual package relying on findutils
coq 8.5.0~camlp4 Formal proof management system.
num 0 The Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.05.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.05.0 Official 4.05.0 release
ocaml-config 1 OCaml Switch Configuration
ocamlbuild 0.14.0 OCamlbuild is a build system with builtin rules to easily build most OCaml projects.
# opam file:
opam-version: "2.0"
maintainer: "vzaliva@cmu.edu"
homepage: "https://github.com/vzaliva/coq-switch"
dev-repo: "git://git@github.com:vzaliva/coq-switch.git"
bug-reports: "https://github.com/vzaliva/coq-switch/issues"
authors: ["Vadim Zaliva <vzaliva@cmu.edu>"]
license: "MIT"
build: [
[make "-j%{jobs}%"]
]
install: [
[make "install"]
]
depends: [
"coq" {>= "8.9.1"}
"coq-metacoq-template" {>= "1.0~alpha+8.9"}
]
tags: [
"category:Miscellaneous/Coq Extensions"
"date:2019-10-09"
"logpath:Switch"
]
synopsis: "A plugin to implement functionality similar to `switch` statement in C language."
description: """It allows easier dispatch on several constant values
of a type with decidable equality. Given a type, boolean equality
predicate, and list of choices, it will generate (using TemplateCoq)
an inductive type with constructors, one for each of the choices, and
a function mapping values to this type."""
url {
src: "https://github.com/vzaliva/coq-switch/archive/v1.0.1.tar.gz"
checksum: "51dc09401a650b0a17c8fa39780fcdb7"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-switch.1.0.1 coq.8.5.0~camlp4[NOTE] Package coq is already installed (current version is 8.5.0~camlp4).
The following dependencies couldn't be met:
- coq-switch -> coq-metacoq-template >= 1.0~alpha+8.9
no matching version
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-switch.1.0.1The following actions will be performed:
- remove coq 8.5.0~camlp4
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[WARNING] While removing coq.8.5.0~camlp4: not removing files that changed since:
- share/emacs/site-lisp/gallina.el
- share/emacs/site-lisp/gallina-syntax.el
- share/emacs/site-lisp/gallina-db.el
- share/emacs/site-lisp/coqdoc.sty
- share/emacs/site-lisp/coq-inferior.el
- share/emacs/site-lisp/coq-font-lock.el
- 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/toploop/tacworkertop.cmxs
- lib/coq/toploop/tacworkertop.cma
- lib/coq/toploop/queryworkertop.cmxs
- lib/coq/toploop/queryworkertop.cma
- lib/coq/toploop/proofworkertop.cmxs
- lib/coq/toploop/proofworkertop.cma
- lib/coq/toploop/coqidetop.cmxs
- lib/coq/toploop/coqidetop.cma
- lib/coq/toplevel/vernacinterp.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.cma
- lib/coq/toplevel/toplevel.a
- lib/coq/toplevel/search.cmi
- lib/coq/toplevel/record.cmi
- lib/coq/toplevel/obligations.cmi
- lib/coq/toplevel/mltop.cmi
- lib/coq/toplevel/metasyntax.cmi
- lib/coq/toplevel/locality.cmi
- lib/coq/toplevel/indschemes.cmi
- lib/coq/toplevel/ind_tables.cmi
- lib/coq/toplevel/himsg.cmi
- lib/coq/toplevel/g_obligations.cmi
- lib/coq/toplevel/discharge.cmi
- lib/coq/toplevel/coqtop.cmi
- lib/coq/toplevel/coqloop.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/auto_ind_decl.cmi
- lib/coq/toplevel/assumptions.cmi
- lib/coq/tools/coqdoc/coqdoc.sty
- lib/coq/tools/coqdoc/coqdoc.css
- lib/coq/tools/compat5.cmo
- lib/coq/theories/ZArith/auxiliary.vo
- lib/coq/theories/ZArith/auxiliary.v
- lib/coq/theories/ZArith/auxiliary.glob
- lib/coq/theories/ZArith/Zwf.vo
- lib/coq/theories/ZArith/Zwf.v
- lib/coq/theories/ZArith/Zwf.glob
- lib/coq/theories/ZArith/Zsqrt_compat.vo
- lib/coq/theories/ZArith/Zsqrt_compat.v
- lib/coq/theories/ZArith/Zsqrt_compat.glob
- lib/coq/theories/ZArith/Zquot.vo
- lib/coq/theories/ZArith/Zquot.v
- lib/coq/theories/ZArith/Zquot.glob
- lib/coq/theories/ZArith/Zpower.vo
- lib/coq/theories/ZArith/Zpower.v
- lib/coq/theories/ZArith/Zpower.glob
- lib/coq/theories/ZArith/Zpow_facts.vo
- lib/coq/theories/ZArith/Zpow_facts.v
- lib/coq/theories/ZArith/Zpow_facts.glob
- lib/coq/theories/ZArith/Zpow_def.vo
- lib/coq/theories/ZArith/Zpow_def.v
- lib/coq/theories/ZArith/Zpow_def.glob
- lib/coq/theories/ZArith/Zpow_alt.vo
- lib/coq/theories/ZArith/Zpow_alt.v
- lib/coq/theories/ZArith/Zpow_alt.glob
- lib/coq/theories/ZArith/Zorder.vo
- lib/coq/theories/ZArith/Zorder.v
- lib/coq/theories/ZArith/Zorder.glob
- lib/coq/theories/ZArith/Znumtheory.vo
- lib/coq/theories/ZArith/Znumtheory.v
- lib/coq/theories/ZArith/Znumtheory.glob
- lib/coq/theories/ZArith/Znat.vo
- lib/coq/theories/ZArith/Znat.v
- lib/coq/theories/ZArith/Znat.glob
- lib/coq/theories/ZArith/Zmisc.vo
- lib/coq/theories/ZArith/Zmisc.v
- lib/coq/theories/ZArith/Zmisc.glob
- lib/coq/theories/ZArith/Zminmax.vo
- lib/coq/theories/ZArith/Zminmax.v
- lib/coq/theories/ZArith/Zminmax.glob
- lib/coq/theories/ZArith/Zmin.vo
- lib/coq/theories/ZArith/Zmin.v
- lib/coq/theories/ZArith/Zmin.glob
- lib/coq/theories/ZArith/Zmax.vo
- lib/coq/theories/ZArith/Zmax.v
- lib/coq/theories/ZArith/Zmax.glob
- lib/coq/theories/ZArith/Zlogarithm.vo
- lib/coq/theories/ZArith/Zlogarithm.v
- lib/coq/theories/ZArith/Zlogarithm.glob
- lib/coq/theories/ZArith/Zhints.vo
- lib/coq/theories/ZArith/Zhints.v
- lib/coq/theories/ZArith/Zhints.glob
- lib/coq/theories/ZArith/Zgcd_alt.vo
- lib/coq/theories/ZArith/Zgcd_alt.v
- lib/coq/theories/ZArith/Zgcd_alt.glob
- lib/coq/theories/ZArith/Zeven.vo
- lib/coq/theories/ZArith/Zeven.v
- lib/coq/theories/ZArith/Zeven.glob
- lib/coq/theories/ZArith/Zeuclid.vo
- lib/coq/theories/ZArith/Zeuclid.v
- lib/coq/theories/ZArith/Zeuclid.glob
- lib/coq/theories/ZArith/Zdiv.vo
- lib/coq/theories/ZArith/Zdiv.v
- lib/coq/theories/ZArith/Zdiv.glob
- lib/coq/theories/ZArith/Zdigits.vo
- lib/coq/theories/ZArith/Zdigits.v
- lib/coq/theories/ZArith/Zdigits.glob
- lib/coq/theories/ZArith/Zcomplements.vo
- lib/coq/theories/ZArith/Zcomplements.v
- lib/coq/theories/ZArith/Zcomplements.glob
- lib/coq/theories/ZArith/Zcompare.vo
- lib/coq/theories/ZArith/Zcompare.v
- lib/coq/theories/ZArith/Zcompare.glob
- lib/coq/theories/ZArith/Zbool.vo
- lib/coq/theories/ZArith/Zbool.v
- lib/coq/theories/ZArith/Zbool.glob
- lib/coq/theories/ZArith/Zabs.vo
- lib/coq/theories/ZArith/Zabs.v
- lib/coq/theories/ZArith/Zabs.glob
- lib/coq/theories/ZArith/ZArith_dec.vo
- lib/coq/theories/ZArith/ZArith_dec.v
- lib/coq/theories/ZArith/ZArith_dec.glob
- lib/coq/theories/ZArith/ZArith_base.vo
- lib/coq/theories/ZArith/ZArith_base.v
- lib/coq/theories/ZArith/ZArith_base.glob
- lib/coq/theories/ZArith/ZArith.vo
- lib/coq/theories/ZArith/ZArith.v
- lib/coq/theories/ZArith/ZArith.glob
- lib/coq/theories/ZArith/Wf_Z.vo
- lib/coq/theories/ZArith/Wf_Z.v
- lib/coq/theories/ZArith/Wf_Z.glob
- lib/coq/theories/ZArith/Int.vo
- lib/coq/theories/ZArith/Int.v
- lib/coq/theories/ZArith/Int.glob
- lib/coq/theories/ZArith/BinIntDef.vo
- lib/coq/theories/ZArith/BinIntDef.v
- lib/coq/theories/ZArith/BinIntDef.glob
- lib/coq/theories/ZArith/BinInt.vo
- lib/coq/theories/ZArith/BinInt.v
- lib/coq/theories/ZArith/BinInt.glob
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_auxiliary.o
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_auxiliary.cmxs
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_auxiliary.cmx
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_auxiliary.cmi
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zwf.o
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zwf.cmxs
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zwf.cmx
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zwf.cmi
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zsqrt_compat.o
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zsqrt_compat.cmxs
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zsqrt_compat.cmx
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zsqrt_compat.cmi
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zquot.o
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zquot.cmxs
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zquot.cmx
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zquot.cmi
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpower.o
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpower.cmxs
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpower.cmx
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpower.cmi
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_facts.o
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_facts.cmxs
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_facts.cmx
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_facts.cmi
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_def.o
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_def.cmxs
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_def.cmx
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_def.cmi
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_alt.o
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_alt.cmxs
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_alt.cmx
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_alt.cmi
- lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zorder.o
[...] truncated
- lib/coq/library/decls.cmi
- lib/coq/library/declaremods.cmi
- lib/coq/library/declare.cmi
- lib/coq/libcoqrun.a
- lib/coq/lib/xml_printer.cmi
- lib/coq/lib/xml_parser.cmi
- lib/coq/lib/xml_lexer.cmi
- lib/coq/lib/xml_datatype.cmi
- lib/coq/lib/util.cmi
- lib/coq/lib/unionfind.cmi
- lib/coq/lib/unicodetable.cmi
- lib/coq/lib/unicode.cmi
- lib/coq/lib/trie.cmi
- lib/coq/lib/terminal.cmi
- lib/coq/lib/system.cmi
- lib/coq/lib/store.cmi
- lib/coq/lib/stateid.cmi
- lib/coq/lib/spawn.cmi
- lib/coq/lib/serialize.cmi
- lib/coq/lib/segmenttree.cmi
- lib/coq/lib/rtree.cmi
- lib/coq/lib/richpp.cmi
- lib/coq/lib/remoteCounter.cmi
- lib/coq/lib/profile.cmi
- lib/coq/lib/predicate.cmi
- lib/coq/lib/ppstyle.cmi
- lib/coq/lib/pp_control.cmi
- lib/coq/lib/pp.cmi
- lib/coq/lib/option.cmi
- lib/coq/lib/monad.cmi
- lib/coq/lib/loc.cmi
- lib/coq/lib/lib.cmxa
- lib/coq/lib/lib.cma
- lib/coq/lib/lib.a
- lib/coq/lib/int.cmi
- lib/coq/lib/iStream.cmi
- lib/coq/lib/hook.cmi
- lib/coq/lib/heap.cmi
- lib/coq/lib/hashset.cmi
- lib/coq/lib/hashcons.cmi
- lib/coq/lib/hMap.cmi
- lib/coq/lib/genarg.cmi
- lib/coq/lib/future.cmi
- lib/coq/lib/flags.cmi
- lib/coq/lib/feedback.cmi
- lib/coq/lib/explore.cmi
- lib/coq/lib/exninfo.cmi
- lib/coq/lib/errors.cmi
- lib/coq/lib/envars.cmi
- lib/coq/lib/dyn.cmi
- lib/coq/lib/deque.cmi
- lib/coq/lib/control.cmi
- lib/coq/lib/clib.cmxa
- lib/coq/lib/clib.cma
- lib/coq/lib/clib.a
- lib/coq/lib/canary.cmi
- lib/coq/lib/cUnix.cmi
- lib/coq/lib/cThread.cmi
- lib/coq/lib/cString.cmi
- lib/coq/lib/cStack.cmi
- lib/coq/lib/cSig.cmi
- lib/coq/lib/cSet.cmi
- lib/coq/lib/cObj.cmi
- lib/coq/lib/cMap.cmi
- lib/coq/lib/cList.cmi
- lib/coq/lib/cEphemeron.cmi
- lib/coq/lib/cArray.cmi
- lib/coq/lib/bigint.cmi
- lib/coq/lib/backtrace.cmi
- lib/coq/lib/aux_file.cmi
- lib/coq/kernel/vm.cmi
- lib/coq/kernel/vconv.cmi
- lib/coq/kernel/vars.cmi
- lib/coq/kernel/univ.cmi
- lib/coq/kernel/uint31.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/sorts.cmi
- lib/coq/kernel/safe_typing.cmi
- lib/coq/kernel/retroknowledge.cmi
- lib/coq/kernel/reduction.cmi
- lib/coq/kernel/primitives.cmi
- lib/coq/kernel/pre_env.cmi
- lib/coq/kernel/opaqueproof.cmi
- lib/coq/kernel/nativevalues.cmi
- lib/coq/kernel/nativelibrary.cmi
- lib/coq/kernel/nativelib.cmi
- lib/coq/kernel/nativelambda.cmi
- lib/coq/kernel/nativeinstr.cmi
- lib/coq/kernel/nativeconv.cmi
- lib/coq/kernel/nativecode.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/fast_typeops.cmi
- lib/coq/kernel/evar.cmi
- lib/coq/kernel/esubst.cmi
- lib/coq/kernel/environ.cmi
- lib/coq/kernel/entries.cmi
- lib/coq/kernel/declareops.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/context.cmi
- lib/coq/kernel/constr.cmi
- lib/coq/kernel/closure.cmi
- lib/coq/kernel/cemitcodes.cmi
- lib/coq/kernel/cbytegen.cmi
- lib/coq/kernel/cbytecodes.cmi
- lib/coq/intf/vernacexpr.cmi
- lib/coq/intf/tacexpr.cmi
- lib/coq/intf/pattern.cmi
- lib/coq/intf/notation_term.cmi
- lib/coq/intf/misctypes.cmi
- lib/coq/intf/locus.cmi
- lib/coq/intf/glob_term.cmi
- lib/coq/intf/genredexpr.cmi
- lib/coq/intf/extend.cmi
- lib/coq/intf/evar_kinds.cmi
- lib/coq/intf/decl_kinds.cmi
- lib/coq/intf/constrexpr.cmi
- lib/coq/interp/topconstr.cmi
- lib/coq/interp/syntax_def.cmi
- lib/coq/interp/stdarg.cmi
- lib/coq/interp/smartlocate.cmi
- lib/coq/interp/reserve.cmi
- lib/coq/interp/ppextend.cmi
- lib/coq/interp/notation_ops.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/genintern.cmi
- lib/coq/interp/dumpglob.cmi
- lib/coq/interp/coqlib.cmi
- lib/coq/interp/constrintern.cmi
- lib/coq/interp/constrextern.cmi
- lib/coq/interp/constrexpr_ops.cmi
- lib/coq/interp/constrarg.cmi
- lib/coq/grammar/q_util.cmi
- lib/coq/grammar/grammar.cma
- lib/coq/dllcoqrun.so
- lib/coq/config/coq_config.cmi
- bin/coqtop.byte
[NOTE] While removing coq.8.5.0~camlp4: not removing non-empty directories:
- share/emacs/site-lisp
- lib/coq/toploop
- lib/coq/toplevel
- lib/coq/tools/coqdoc
- lib/coq/theories/ZArith/.coq-native
- lib/coq/theories/Wellfounded/.coq-native
- lib/coq/theories/Vectors/.coq-native
- lib/coq/theories/Unicode/.coq-native
- lib/coq/theories/Structures/.coq-native
- lib/coq/theories/Strings/.coq-native
- lib/coq/theories/Sorting/.coq-native
- lib/coq/theories/Sets/.coq-native
- lib/coq/theories/Setoids/.coq-native
- lib/coq/theories/Relations/.coq-native
- lib/coq/theories/Reals/.coq-native
- lib/coq/theories/QArith/.coq-native
- lib/coq/theories/Program/.coq-native
- lib/coq/theories/PArith/.coq-native
- lib/coq/theories/Numbers/Rational/SpecViaQ/.coq-native
- lib/coq/theories/Numbers/Rational/BigQ/.coq-native
- lib/coq/theories/Numbers/Natural/SpecViaZ/.coq-native
- lib/coq/theories/Numbers/Natural/Peano/.coq-native
- lib/coq/theories/Numbers/Natural/Binary/.coq-native
- lib/coq/theories/Numbers/Natural/BigN/.coq-native
- lib/coq/theories/Numbers/Natural/Abstract/.coq-native
- lib/coq/theories/Numbers/NatInt/.coq-native
- lib/coq/theories/Numbers/Integer/SpecViaZ/.coq-native
- lib/coq/theories/Numbers/Integer/NatPairs/.coq-native
- lib/coq/theories/Numbers/Integer/Binary/.coq-native
- lib/coq/theories/Numbers/Integer/BigZ/.coq-native
- lib/coq/theories/Numbers/Integer/Abstract/.coq-native
- lib/coq/theories/Numbers/Cyclic/ZModulo/.coq-native
- lib/coq/theories/Numbers/Cyclic/Int31/.coq-native
- lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native
- lib/coq/theories/Numbers/Cyclic/Abstract/.coq-native
- lib/coq/theories/Numbers/.coq-native
- lib/coq/theories/NArith/.coq-native
- lib/coq/theories/MSets/.coq-native
- lib/coq/theories/Logic/.coq-native
- lib/coq/theories/Lists/.coq-native
- lib/coq/theories/Init/.coq-native
- lib/coq/theories/FSets/.coq-native
- lib/coq/theories/Compat/.coq-native
- lib/coq/theories/Classes/.coq-native
- lib/coq/theories/Bool/.coq-native
- lib/coq/theories/Arith/.coq-native
- lib/coq/tactics
- lib/coq/stm
- lib/coq/proofs
- lib/coq/printing
- lib/coq/pretyping
- lib/coq/plugins/syntax
- lib/coq/plugins/setoid_ring/.coq-native
- lib/coq/plugins/rtauto/.coq-native
- lib/coq/plugins/romega/.coq-native
- lib/coq/plugins/quote/.coq-native
- lib/coq/plugins/omega/.coq-native
- lib/coq/plugins/nsatz/.coq-native
- lib/coq/plugins/micromega/.coq-native
- lib/coq/plugins/funind/.coq-native
- lib/coq/plugins/fourier/.coq-native
- lib/coq/plugins/firstorder
- lib/coq/plugins/extraction/.coq-native
- lib/coq/plugins/derive/.coq-native
- lib/coq/plugins/decl_mode
- lib/coq/plugins/cc
- lib/coq/plugins/btauto/.coq-native
- lib/coq/parsing
- lib/coq/library
- lib/coq/kernel
- lib/coq/intf
- lib/coq/interp
- lib/coq/grammar
- lib/coq/config
-> removed coq.8.5.0~camlp4
Done.
# Run eval $(opam env) to update the current shell environment
The following dependencies couldn't be met:
- coq-switch -> coq-metacoq-template >= 1.0~alpha+8.9
no matching version
No solution found, exiting
The middle of the output is truncated (maximum 20000 characters)
truetrueNo files were installed.
true