Date: Sat, 31 Dec 2016 23:05:09 +0000 (UTC) From: Hiroki Sato <hrs@FreeBSD.org> To: ports-committers@freebsd.org, svn-ports-all@freebsd.org, svn-ports-head@freebsd.org Subject: svn commit: r430173 - in head/math/coq: . files Message-ID: <201612312305.uBVN59uL045254@repo.freebsd.org>
next in thread | raw e-mail | index | archive | help
Author: hrs Date: Sat Dec 31 23:05:08 2016 New Revision: 430173 URL: https://svnweb.freebsd.org/changeset/ports/430173 Log: Update to 8.6. Fix PORTEPOCH accidentally removed in the previous commit. Added: head/math/coq/files/patch-Makefile.install - copied, changed from r430124, head/math/coq/files/patch-Makefile.build Deleted: head/math/coq/files/patch-configure.ml Modified: head/math/coq/Makefile head/math/coq/distinfo head/math/coq/files/patch-Makefile.build head/math/coq/pkg-plist Modified: head/math/coq/Makefile ============================================================================== --- head/math/coq/Makefile Sat Dec 31 22:22:01 2016 (r430172) +++ head/math/coq/Makefile Sat Dec 31 23:05:08 2016 (r430173) @@ -1,7 +1,8 @@ # $FreeBSD$ PORTNAME= coq -PORTVERSION= 8.5 +PORTVERSION= 8.6 +PORTEPOCH= 3 CATEGORIES= math MASTER_SITES= http://coq.inria.fr/distrib/V${PORTVERSION}/files/ \ ftp://ftp.stack.nl/pub/users/johans/coq/ @@ -17,7 +18,6 @@ BUILD_DEPENDS= camlp5:devel/ocaml-camlp5 LIB_DEPENDS= libfontconfig.so:x11-fonts/fontconfig \ libfreetype.so:print/freetype2 -COQVERSION= ${PORTVERSION:R}pl${PORTVERSION:E} USES= gmake gettext-runtime USE_EMACS= yes USE_GNOME= atk cairo gdkpixbuf2 glib20 gtk20 gtksourceview2 pango @@ -28,8 +28,7 @@ CONFIGURE_ARGS= -prefix ${PREFIX} \ -mandir ${PREFIX}/man \ -emacslib ${PREFIX}/share/emacs/site-lisp/coq \ -usecamlp5 \ - -byteonly \ - -makecmd ${MAKE_CMD} + -byteonly MAKE_ENV= VERBOSE=1 ALL_TARGET= world Modified: head/math/coq/distinfo ============================================================================== --- head/math/coq/distinfo Sat Dec 31 22:22:01 2016 (r430172) +++ head/math/coq/distinfo Sat Dec 31 23:05:08 2016 (r430173) @@ -1,3 +1,3 @@ -TIMESTAMP = 1483174912 -SHA256 (coq-8.5.tar.gz) = 89a92fb8b91e7cb0797d41c87cd13e4b63bee76c32a6dcc3d7c8055ca6a9ae3d -SIZE (coq-8.5.tar.gz) = 5346653 +TIMESTAMP = 1483223265 +SHA256 (coq-8.6.tar.gz) = 6e3c3cf5c8e2b0b760dc52738e2e849f3a8c630869659ecc0cf41413fcee81df +SIZE (coq-8.6.tar.gz) = 5538848 Modified: head/math/coq/files/patch-Makefile.build ============================================================================== --- head/math/coq/files/patch-Makefile.build Sat Dec 31 22:22:01 2016 (r430172) +++ head/math/coq/files/patch-Makefile.build Sat Dec 31 23:05:08 2016 (r430173) @@ -1,29 +1,11 @@ ---- Makefile.build.orig 2016-01-20 16:52:18 UTC +--- Makefile.build.orig 2016-12-08 15:13:52 UTC +++ Makefile.build -@@ -56,7 +56,7 @@ CURDEPS:=$(addsuffix .d, $(CURFILES)) +@@ -101,7 +101,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMEC + # TIME="%C (%U user, %S sys, %e total, %M maxres)" - # Variables meant to be modifiable via the command-line of make - --VERBOSE= -+VERBOSE=1 - NO_RECOMPILE_ML4= - NO_RECALC_DEPS= - READABLE_ML4= # non-empty means .ml of .ml4 will be ascii instead of binary -@@ -82,7 +82,7 @@ STDTIME=/usr/bin/time -f "$* (user: %U m - TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) - - COQOPTS=$(COQ_XML) $(VM) $(NATIVECOMPUTE) + COQOPTS=$(COQ_XML) $(NATIVECOMPUTE) -BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile +BOOTCOQC=$(TIMER) env CAML_LD_LIBRARY_PATH=$${PWD}/kernel/byterun $(COQTOPEXE) -boot $(COQOPTS) -compile - # The SHOW and HIDE variables control whether make will echo complete commands - # or only abbreviated versions. -@@ -704,7 +704,7 @@ install-doc-no: - .PHONY: install install-doc-all install-doc-no - - #These variables are intended to be set by the caller to make --#COQINSTALLPREFIX= -+COQINSTALLPREFIX=${DESTDIR} - #OLDROOT= - - # Can be changed for a local installation (to make packages). + LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) ) + MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) Copied and modified: head/math/coq/files/patch-Makefile.install (from r430124, head/math/coq/files/patch-Makefile.build) ============================================================================== --- head/math/coq/files/patch-Makefile.build Sat Dec 31 14:32:50 2016 (r430124, copy source) +++ head/math/coq/files/patch-Makefile.install Sat Dec 31 23:05:08 2016 (r430173) @@ -1,24 +1,6 @@ ---- Makefile.build.orig 2016-01-20 16:52:18 UTC -+++ Makefile.build -@@ -56,7 +56,7 @@ CURDEPS:=$(addsuffix .d, $(CURFILES)) - - # Variables meant to be modifiable via the command-line of make - --VERBOSE= -+VERBOSE=1 - NO_RECOMPILE_ML4= - NO_RECALC_DEPS= - READABLE_ML4= # non-empty means .ml of .ml4 will be ascii instead of binary -@@ -82,7 +82,7 @@ STDTIME=/usr/bin/time -f "$* (user: %U m - TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) - - COQOPTS=$(COQ_XML) $(VM) $(NATIVECOMPUTE) --BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile -+BOOTCOQC=$(TIMER) env CAML_LD_LIBRARY_PATH=$${PWD}/kernel/byterun $(COQTOPEXE) -boot $(COQOPTS) -compile - - # The SHOW and HIDE variables control whether make will echo complete commands - # or only abbreviated versions. -@@ -704,7 +704,7 @@ install-doc-no: +--- Makefile.install.orig 2016-12-08 15:13:52 UTC ++++ Makefile.install +@@ -29,7 +29,7 @@ install-doc-no: .PHONY: install install-doc-all install-doc-no #These variables are intended to be set by the caller to make Modified: head/math/coq/pkg-plist ============================================================================== --- head/math/coq/pkg-plist Sat Dec 31 22:22:01 2016 (r430172) +++ head/math/coq/pkg-plist Sat Dec 31 23:05:08 2016 (r430173) @@ -11,8 +11,22 @@ bin/coqtop.byte bin/coqwc bin/coqworkmgr bin/gallina +lib/coq/META lib/coq/config/coq_config.cmi lib/coq/dllcoqrun.so +lib/coq/engine/engine.cma +lib/coq/engine/evarutil.cmi +lib/coq/engine/evd.cmi +lib/coq/engine/ftactic.cmi +lib/coq/engine/geninterp.cmi +lib/coq/engine/logic_monad.cmi +lib/coq/engine/namegen.cmi +lib/coq/engine/proofview.cmi +lib/coq/engine/proofview_monad.cmi +lib/coq/engine/sigma.cmi +lib/coq/engine/termops.cmi +lib/coq/engine/uState.cmi +lib/coq/grammar/compat5.cmo lib/coq/grammar/grammar.cma lib/coq/grammar/q_util.cmi %%IDE%%lib/coq/ide/config_lexer.cmi @@ -31,7 +45,9 @@ lib/coq/grammar/q_util.cmi %%IDE%%lib/coq/ide/nanoPG.cmi %%IDE%%lib/coq/ide/preferences.cmi %%IDE%%lib/coq/ide/project_file.cmi +%%IDE%%lib/coq/ide/richprinter.cmi %%IDE%%lib/coq/ide/sentence.cmi +%%IDE%%lib/coq/ide/serialize.cmi %%IDE%%lib/coq/ide/session.cmi %%IDE%%lib/coq/ide/tags.cmi %%IDE%%lib/coq/ide/utf8_convert.cmi @@ -52,6 +68,9 @@ lib/coq/grammar/q_util.cmi %%IDE%%lib/coq/ide/wg_ProofView.cmi %%IDE%%lib/coq/ide/wg_ScriptView.cmi %%IDE%%lib/coq/ide/wg_Segment.cmi +%%IDE%%lib/coq/ide/xml_lexer.cmi +%%IDE%%lib/coq/ide/xml_parser.cmi +%%IDE%%lib/coq/ide/xml_printer.cmi %%IDE%%lib/coq/ide/xmlprotocol.cmi lib/coq/interp/constrarg.cmi lib/coq/interp/constrexpr_ops.cmi @@ -83,10 +102,10 @@ lib/coq/intf/notation_term.cmi lib/coq/intf/pattern.cmi lib/coq/intf/tacexpr.cmi lib/coq/intf/vernacexpr.cmi +lib/coq/kernel/cClosure.cmi lib/coq/kernel/cbytecodes.cmi lib/coq/kernel/cbytegen.cmi lib/coq/kernel/cemitcodes.cmi -lib/coq/kernel/closure.cmi lib/coq/kernel/constr.cmi lib/coq/kernel/context.cmi lib/coq/kernel/conv_oracle.cmi @@ -126,6 +145,7 @@ lib/coq/kernel/term.cmi lib/coq/kernel/term_typing.cmi lib/coq/kernel/type_errors.cmi lib/coq/kernel/typeops.cmi +lib/coq/kernel/uGraph.cmi lib/coq/kernel/uint31.cmi lib/coq/kernel/univ.cmi lib/coq/kernel/vars.cmi @@ -135,6 +155,8 @@ lib/coq/lib/aux_file.cmi lib/coq/lib/backtrace.cmi lib/coq/lib/bigint.cmi lib/coq/lib/cArray.cmi +lib/coq/lib/cEphemeron.cmi +lib/coq/lib/cErrors.cmi lib/coq/lib/cList.cmi lib/coq/lib/cMap.cmi lib/coq/lib/cObj.cmi @@ -144,14 +166,13 @@ lib/coq/lib/cStack.cmi lib/coq/lib/cString.cmi lib/coq/lib/cThread.cmi lib/coq/lib/cUnix.cmi +lib/coq/lib/cWarnings.cmi lib/coq/lib/canary.cmi lib/coq/lib/clib.cma lib/coq/lib/control.cmi lib/coq/lib/deque.cmi lib/coq/lib/dyn.cmi lib/coq/lib/envars.cmi -lib/coq/lib/ephemeron.cmi -lib/coq/lib/errors.cmi lib/coq/lib/exninfo.cmi lib/coq/lib/explore.cmi lib/coq/lib/feedback.cmi @@ -167,6 +188,7 @@ lib/coq/lib/iStream.cmi lib/coq/lib/int.cmi lib/coq/lib/lib.cma lib/coq/lib/loc.cmi +lib/coq/lib/minisys.cmi lib/coq/lib/monad.cmi lib/coq/lib/option.cmi lib/coq/lib/pp.cmi @@ -178,7 +200,6 @@ lib/coq/lib/remoteCounter.cmi lib/coq/lib/richpp.cmi lib/coq/lib/rtree.cmi lib/coq/lib/segmenttree.cmi -lib/coq/lib/serialize.cmi lib/coq/lib/spawn.cmi lib/coq/lib/stateid.cmi lib/coq/lib/store.cmi @@ -190,9 +211,6 @@ lib/coq/lib/unicodetable.cmi lib/coq/lib/unionfind.cmi lib/coq/lib/util.cmi lib/coq/lib/xml_datatype.cmi -lib/coq/lib/xml_lexer.cmi -lib/coq/lib/xml_parser.cmi -lib/coq/lib/xml_printer.cmi lib/coq/library/declare.cmi lib/coq/library/declaremods.cmi lib/coq/library/decls.cmi @@ -215,17 +233,39 @@ lib/coq/library/nametab.cmi lib/coq/library/states.cmi lib/coq/library/summary.cmi lib/coq/library/universes.cmi +lib/coq/ltac/coretactics.cmi +lib/coq/ltac/evar_tactics.cmi +lib/coq/ltac/extraargs.cmi +lib/coq/ltac/extratactics.cmi +lib/coq/ltac/g_auto.cmi +lib/coq/ltac/g_class.cmi +lib/coq/ltac/g_eqdecide.cmi +lib/coq/ltac/g_ltac.cmi +lib/coq/ltac/g_obligations.cmi +lib/coq/ltac/g_rewrite.cmi +lib/coq/ltac/ltac.cma +lib/coq/ltac/profile_ltac.cmi +lib/coq/ltac/profile_ltac_tactics.cmi +lib/coq/ltac/rewrite.cmi +lib/coq/ltac/taccoerce.cmi +lib/coq/ltac/tacentries.cmi +lib/coq/ltac/tacenv.cmi +lib/coq/ltac/tacintern.cmi +lib/coq/ltac/tacinterp.cmi +lib/coq/ltac/tacsubst.cmi +lib/coq/ltac/tactic_debug.cmi +lib/coq/ltac/tactic_option.cmi +lib/coq/ltac/tauto.cmi +lib/coq/parsing/cLexer.cmi lib/coq/parsing/compat.cmi lib/coq/parsing/egramcoq.cmi lib/coq/parsing/egramml.cmi lib/coq/parsing/g_constr.cmi -lib/coq/parsing/g_ltac.cmi lib/coq/parsing/g_prim.cmi lib/coq/parsing/g_proofs.cmi lib/coq/parsing/g_tactic.cmi lib/coq/parsing/g_vernac.cmi lib/coq/parsing/highparsing.cma -lib/coq/parsing/lexer.cmi lib/coq/parsing/parsing.cma lib/coq/parsing/pcoq.cmi lib/coq/parsing/tok.cmi @@ -244,23 +284,19 @@ lib/coq/plugins/btauto/Btauto.vo lib/coq/plugins/btauto/Reflect.glob lib/coq/plugins/btauto/Reflect.v lib/coq/plugins/btauto/Reflect.vo -lib/coq/plugins/btauto/btauto_plugin.cma -lib/coq/plugins/btauto/btauto_plugin_mod.cmi -lib/coq/plugins/btauto/g_btauto.cmi -lib/coq/plugins/btauto/refl_btauto.cmi -lib/coq/plugins/cc/cc_plugin.cma -lib/coq/plugins/cc/cc_plugin_mod.cmi +lib/coq/plugins/btauto/btauto_plugin.cmi +lib/coq/plugins/btauto/btauto_plugin.cmo +lib/coq/plugins/cc/cc_plugin.cmi +lib/coq/plugins/cc/cc_plugin.cmo lib/coq/plugins/cc/ccalgo.cmi lib/coq/plugins/cc/ccproof.cmi lib/coq/plugins/cc/cctac.cmi -lib/coq/plugins/cc/g_congruence.cmi lib/coq/plugins/decl_mode/decl_expr.cmi lib/coq/plugins/decl_mode/decl_interp.cmi lib/coq/plugins/decl_mode/decl_mode.cmi -lib/coq/plugins/decl_mode/decl_mode_plugin.cma -lib/coq/plugins/decl_mode/decl_mode_plugin_mod.cmi +lib/coq/plugins/decl_mode/decl_mode_plugin.cmi +lib/coq/plugins/decl_mode/decl_mode_plugin.cmo lib/coq/plugins/decl_mode/decl_proof_instr.cmi -lib/coq/plugins/decl_mode/g_decl_mode.cmi lib/coq/plugins/decl_mode/ppdecl_proof.cmi lib/coq/plugins/derive/.coq-native/NCoq_derive_Derive.cmi lib/coq/plugins/derive/.coq-native/NCoq_derive_Derive.cmo @@ -268,8 +304,8 @@ lib/coq/plugins/derive/Derive.glob lib/coq/plugins/derive/Derive.v lib/coq/plugins/derive/Derive.vo lib/coq/plugins/derive/derive.cmi -lib/coq/plugins/derive/derive_plugin.cma -lib/coq/plugins/derive/g_derive.cmi +lib/coq/plugins/derive/derive_plugin.cmi +lib/coq/plugins/derive/derive_plugin.cmo lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.cmi lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.cmo lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInt.cmi @@ -353,9 +389,8 @@ lib/coq/plugins/extraction/ExtrOcamlZInt lib/coq/plugins/extraction/common.cmi lib/coq/plugins/extraction/extract_env.cmi lib/coq/plugins/extraction/extraction.cmi -lib/coq/plugins/extraction/extraction_plugin.cma -lib/coq/plugins/extraction/extraction_plugin_mod.cmi -lib/coq/plugins/extraction/g_extraction.cmi +lib/coq/plugins/extraction/extraction_plugin.cmi +lib/coq/plugins/extraction/extraction_plugin.cmo lib/coq/plugins/extraction/haskell.cmi lib/coq/plugins/extraction/json.cmi lib/coq/plugins/extraction/miniml.cmi @@ -365,10 +400,9 @@ lib/coq/plugins/extraction/ocaml.cmi lib/coq/plugins/extraction/scheme.cmi lib/coq/plugins/extraction/table.cmi lib/coq/plugins/firstorder/formula.cmi -lib/coq/plugins/firstorder/g_ground.cmi lib/coq/plugins/firstorder/ground.cmi -lib/coq/plugins/firstorder/ground_plugin.cma -lib/coq/plugins/firstorder/ground_plugin_mod.cmi +lib/coq/plugins/firstorder/ground_plugin.cmi +lib/coq/plugins/firstorder/ground_plugin.cmo lib/coq/plugins/firstorder/instances.cmi lib/coq/plugins/firstorder/rules.cmi lib/coq/plugins/firstorder/sequent.cmi @@ -383,11 +417,8 @@ lib/coq/plugins/fourier/Fourier.vo lib/coq/plugins/fourier/Fourier_util.glob lib/coq/plugins/fourier/Fourier_util.v lib/coq/plugins/fourier/Fourier_util.vo -lib/coq/plugins/fourier/fourier.cmi -lib/coq/plugins/fourier/fourierR.cmi -lib/coq/plugins/fourier/fourier_plugin.cma -lib/coq/plugins/fourier/fourier_plugin_mod.cmi -lib/coq/plugins/fourier/g_fourier.cmi +lib/coq/plugins/fourier/fourier_plugin.cmi +lib/coq/plugins/fourier/fourier_plugin.cmo lib/coq/plugins/funind/.coq-native/NCoq_funind_Recdef.cmi lib/coq/plugins/funind/.coq-native/NCoq_funind_Recdef.cmo lib/coq/plugins/funind/Recdef.glob @@ -395,22 +426,23 @@ lib/coq/plugins/funind/Recdef.v lib/coq/plugins/funind/Recdef.vo lib/coq/plugins/funind/functional_principles_proofs.cmi lib/coq/plugins/funind/functional_principles_types.cmi -lib/coq/plugins/funind/g_indfun.cmi lib/coq/plugins/funind/glob_term_to_relation.cmi lib/coq/plugins/funind/glob_termops.cmi lib/coq/plugins/funind/indfun.cmi lib/coq/plugins/funind/indfun_common.cmi -lib/coq/plugins/funind/invfun.cmi -lib/coq/plugins/funind/merge.cmi lib/coq/plugins/funind/recdef.cmi -lib/coq/plugins/funind/recdef_plugin.cma -lib/coq/plugins/funind/recdef_plugin_mod.cmi +lib/coq/plugins/funind/recdef_plugin.cmi +lib/coq/plugins/funind/recdef_plugin.cmo lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmi lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmo lib/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.cmi lib/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.cmo lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lia.cmi lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lia.cmo +lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lqa.cmi +lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lqa.cmo +lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lra.cmi +lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lra.cmo lib/coq/plugins/micromega/.coq-native/NCoq_micromega_OrderedRing.cmi lib/coq/plugins/micromega/.coq-native/NCoq_micromega_OrderedRing.cmo lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Psatz.cmi @@ -440,6 +472,12 @@ lib/coq/plugins/micromega/EnvRing.vo lib/coq/plugins/micromega/Lia.glob lib/coq/plugins/micromega/Lia.v lib/coq/plugins/micromega/Lia.vo +lib/coq/plugins/micromega/Lqa.glob +lib/coq/plugins/micromega/Lqa.v +lib/coq/plugins/micromega/Lqa.vo +lib/coq/plugins/micromega/Lra.glob +lib/coq/plugins/micromega/Lra.v +lib/coq/plugins/micromega/Lra.vo lib/coq/plugins/micromega/OrderedRing.glob lib/coq/plugins/micromega/OrderedRing.v lib/coq/plugins/micromega/OrderedRing.vo @@ -470,19 +508,11 @@ lib/coq/plugins/micromega/ZCoeff.vo lib/coq/plugins/micromega/ZMicromega.glob lib/coq/plugins/micromega/ZMicromega.v lib/coq/plugins/micromega/ZMicromega.vo -lib/coq/plugins/micromega/certificate.cmi -lib/coq/plugins/micromega/coq_micromega.cmi lib/coq/plugins/micromega/csdpcert -lib/coq/plugins/micromega/g_micromega.cmi -lib/coq/plugins/micromega/mfourier.cmi lib/coq/plugins/micromega/micromega.cmi -lib/coq/plugins/micromega/micromega_plugin.cma -lib/coq/plugins/micromega/micromega_plugin_mod.cmi -lib/coq/plugins/micromega/mutils.cmi -lib/coq/plugins/micromega/persistent_cache.cmi -lib/coq/plugins/micromega/polynomial.cmi +lib/coq/plugins/micromega/micromega_plugin.cmi +lib/coq/plugins/micromega/micromega_plugin.cmo lib/coq/plugins/micromega/sos.cmi -lib/coq/plugins/micromega/sos_types.cmi lib/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmi lib/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmo lib/coq/plugins/nsatz/Nsatz.glob @@ -490,8 +520,8 @@ lib/coq/plugins/nsatz/Nsatz.v lib/coq/plugins/nsatz/Nsatz.vo lib/coq/plugins/nsatz/ideal.cmi lib/coq/plugins/nsatz/nsatz.cmi -lib/coq/plugins/nsatz/nsatz_plugin.cma -lib/coq/plugins/nsatz/nsatz_plugin_mod.cmi +lib/coq/plugins/nsatz/nsatz_plugin.cmi +lib/coq/plugins/nsatz/nsatz_plugin.cmo lib/coq/plugins/nsatz/polynom.cmi lib/coq/plugins/nsatz/utile.cmi lib/coq/plugins/omega/.coq-native/NCoq_omega_Omega.cmi @@ -519,20 +549,15 @@ lib/coq/plugins/omega/OmegaTactic.vo lib/coq/plugins/omega/PreOmega.glob lib/coq/plugins/omega/PreOmega.v lib/coq/plugins/omega/PreOmega.vo -lib/coq/plugins/omega/coq_omega.cmi -lib/coq/plugins/omega/g_omega.cmi -lib/coq/plugins/omega/omega.cmi -lib/coq/plugins/omega/omega_plugin.cma -lib/coq/plugins/omega/omega_plugin_mod.cmi +lib/coq/plugins/omega/omega_plugin.cmi +lib/coq/plugins/omega/omega_plugin.cmo lib/coq/plugins/quote/.coq-native/NCoq_quote_Quote.cmi lib/coq/plugins/quote/.coq-native/NCoq_quote_Quote.cmo lib/coq/plugins/quote/Quote.glob lib/coq/plugins/quote/Quote.v lib/coq/plugins/quote/Quote.vo -lib/coq/plugins/quote/g_quote.cmi -lib/coq/plugins/quote/quote.cmi -lib/coq/plugins/quote/quote_plugin.cma -lib/coq/plugins/quote/quote_plugin_mod.cmi +lib/coq/plugins/quote/quote_plugin.cmi +lib/coq/plugins/quote/quote_plugin.cmo lib/coq/plugins/romega/.coq-native/NCoq_romega_ROmega.cmi lib/coq/plugins/romega/.coq-native/NCoq_romega_ROmega.cmo lib/coq/plugins/romega/.coq-native/NCoq_romega_ReflOmegaCore.cmi @@ -544,10 +569,8 @@ lib/coq/plugins/romega/ReflOmegaCore.glo lib/coq/plugins/romega/ReflOmegaCore.v lib/coq/plugins/romega/ReflOmegaCore.vo lib/coq/plugins/romega/const_omega.cmi -lib/coq/plugins/romega/g_romega.cmi -lib/coq/plugins/romega/refl_omega.cmi -lib/coq/plugins/romega/romega_plugin.cma -lib/coq/plugins/romega/romega_plugin_mod.cmi +lib/coq/plugins/romega/romega_plugin.cmi +lib/coq/plugins/romega/romega_plugin.cmo lib/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.cmi lib/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.cmo lib/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Rtauto.cmi @@ -558,11 +581,10 @@ lib/coq/plugins/rtauto/Bintree.vo lib/coq/plugins/rtauto/Rtauto.glob lib/coq/plugins/rtauto/Rtauto.v lib/coq/plugins/rtauto/Rtauto.vo -lib/coq/plugins/rtauto/g_rtauto.cmi lib/coq/plugins/rtauto/proof_search.cmi lib/coq/plugins/rtauto/refl_tauto.cmi -lib/coq/plugins/rtauto/rtauto_plugin.cma -lib/coq/plugins/rtauto/rtauto_plugin_mod.cmi +lib/coq/plugins/rtauto/rtauto_plugin.cmi +lib/coq/plugins/rtauto/rtauto_plugin.cmo lib/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Algebra_syntax.cmi lib/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Algebra_syntax.cmo lib/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_ArithRing.cmi @@ -684,26 +706,29 @@ lib/coq/plugins/setoid_ring/ZArithRing.g lib/coq/plugins/setoid_ring/ZArithRing.v lib/coq/plugins/setoid_ring/ZArithRing.vo lib/coq/plugins/setoid_ring/newring.cmi -lib/coq/plugins/setoid_ring/newring_plugin.cma -lib/coq/plugins/setoid_ring/newring_plugin_mod.cmi -lib/coq/plugins/syntax/ascii_syntax.cmi -lib/coq/plugins/syntax/ascii_syntax_plugin.cma -lib/coq/plugins/syntax/ascii_syntax_plugin_mod.cmi -lib/coq/plugins/syntax/nat_syntax.cmi -lib/coq/plugins/syntax/nat_syntax_plugin.cma -lib/coq/plugins/syntax/nat_syntax_plugin_mod.cmi -lib/coq/plugins/syntax/numbers_syntax.cmi -lib/coq/plugins/syntax/numbers_syntax_plugin.cma -lib/coq/plugins/syntax/numbers_syntax_plugin_mod.cmi -lib/coq/plugins/syntax/r_syntax.cmi -lib/coq/plugins/syntax/r_syntax_plugin.cma -lib/coq/plugins/syntax/r_syntax_plugin_mod.cmi -lib/coq/plugins/syntax/string_syntax.cmi -lib/coq/plugins/syntax/string_syntax_plugin.cma -lib/coq/plugins/syntax/string_syntax_plugin_mod.cmi -lib/coq/plugins/syntax/z_syntax.cmi -lib/coq/plugins/syntax/z_syntax_plugin.cma -lib/coq/plugins/syntax/z_syntax_plugin_mod.cmi +lib/coq/plugins/setoid_ring/newring_ast.cmi +lib/coq/plugins/setoid_ring/newring_plugin.cmi +lib/coq/plugins/setoid_ring/newring_plugin.cmo +lib/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmi +lib/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmo +lib/coq/plugins/ssrmatching/ssrmatching.cmi +lib/coq/plugins/ssrmatching/ssrmatching.glob +lib/coq/plugins/ssrmatching/ssrmatching.v +lib/coq/plugins/ssrmatching/ssrmatching.vo +lib/coq/plugins/ssrmatching/ssrmatching_plugin.cmi +lib/coq/plugins/ssrmatching/ssrmatching_plugin.cmo +lib/coq/plugins/syntax/ascii_syntax_plugin.cmi +lib/coq/plugins/syntax/ascii_syntax_plugin.cmo +lib/coq/plugins/syntax/nat_syntax_plugin.cmi +lib/coq/plugins/syntax/nat_syntax_plugin.cmo +lib/coq/plugins/syntax/numbers_syntax_plugin.cmi +lib/coq/plugins/syntax/numbers_syntax_plugin.cmo +lib/coq/plugins/syntax/r_syntax_plugin.cmi +lib/coq/plugins/syntax/r_syntax_plugin.cmo +lib/coq/plugins/syntax/string_syntax_plugin.cmi +lib/coq/plugins/syntax/string_syntax_plugin.cmo +lib/coq/plugins/syntax/z_syntax_plugin.cmi +lib/coq/plugins/syntax/z_syntax_plugin.cmo lib/coq/pretyping/arguments_renaming.cmi lib/coq/pretyping/cases.cmi lib/coq/pretyping/cbv.cmi @@ -712,16 +737,14 @@ lib/coq/pretyping/coercion.cmi lib/coq/pretyping/constr_matching.cmi lib/coq/pretyping/detyping.cmi lib/coq/pretyping/evarconv.cmi +lib/coq/pretyping/evardefine.cmi lib/coq/pretyping/evarsolve.cmi -lib/coq/pretyping/evarutil.cmi -lib/coq/pretyping/evd.cmi lib/coq/pretyping/find_subterm.cmi lib/coq/pretyping/glob_ops.cmi lib/coq/pretyping/indrec.cmi lib/coq/pretyping/inductiveops.cmi lib/coq/pretyping/locusops.cmi lib/coq/pretyping/miscops.cmi -lib/coq/pretyping/namegen.cmi lib/coq/pretyping/nativenorm.cmi lib/coq/pretyping/patternops.cmi lib/coq/pretyping/pretype_errors.cmi @@ -733,7 +756,6 @@ lib/coq/pretyping/redops.cmi lib/coq/pretyping/reductionops.cmi lib/coq/pretyping/retyping.cmi lib/coq/pretyping/tacred.cmi -lib/coq/pretyping/termops.cmi lib/coq/pretyping/typeclasses.cmi lib/coq/pretyping/typeclasses_errors.cmi lib/coq/pretyping/typing.cmi @@ -754,34 +776,30 @@ lib/coq/printing/printer.cmi lib/coq/printing/printing.cma lib/coq/printing/printmod.cmi lib/coq/printing/printmodsig.cmi -lib/coq/printing/richprinter.cmi lib/coq/proofs/clenv.cmi lib/coq/proofs/clenvtac.cmi lib/coq/proofs/evar_refiner.cmi lib/coq/proofs/goal.cmi lib/coq/proofs/logic.cmi -lib/coq/proofs/logic_monad.cmi lib/coq/proofs/pfedit.cmi lib/coq/proofs/proof.cmi lib/coq/proofs/proof_global.cmi lib/coq/proofs/proof_type.cmi lib/coq/proofs/proof_using.cmi lib/coq/proofs/proofs.cma -lib/coq/proofs/proofview.cmi -lib/coq/proofs/proofview_monad.cmi lib/coq/proofs/redexpr.cmi +lib/coq/proofs/refine.cmi lib/coq/proofs/refiner.cmi lib/coq/proofs/tacmach.cmi -lib/coq/proofs/tactic_debug.cmi lib/coq/stm/asyncTaskQueue.cmi lib/coq/stm/coqworkmgrApi.cmi lib/coq/stm/dag.cmi lib/coq/stm/lemmas.cmi +lib/coq/stm/proofBlockDelimiter.cmi lib/coq/stm/spawned.cmi lib/coq/stm/stm.cma lib/coq/stm/stm.cmi lib/coq/stm/tQueue.cmi -lib/coq/stm/texmacspp.cmi lib/coq/stm/vcs.cmi lib/coq/stm/vernac_classifier.cmi lib/coq/stm/vio_checking.cmi @@ -791,7 +809,6 @@ lib/coq/tactics/autorewrite.cmi lib/coq/tactics/btermdn.cmi lib/coq/tactics/class_tactics.cmi lib/coq/tactics/contradiction.cmi -lib/coq/tactics/coretactics.cmi lib/coq/tactics/dn.cmi lib/coq/tactics/dnet.cmi lib/coq/tactics/eauto.cmi @@ -800,31 +817,14 @@ lib/coq/tactics/elimschemes.cmi lib/coq/tactics/eqdecide.cmi lib/coq/tactics/eqschemes.cmi lib/coq/tactics/equality.cmi -lib/coq/tactics/evar_tactics.cmi -lib/coq/tactics/extraargs.cmi -lib/coq/tactics/extratactics.cmi -lib/coq/tactics/ftactic.cmi -lib/coq/tactics/g_class.cmi -lib/coq/tactics/g_eqdecide.cmi -lib/coq/tactics/g_rewrite.cmi -lib/coq/tactics/geninterp.cmi -lib/coq/tactics/hightactics.cma lib/coq/tactics/hints.cmi lib/coq/tactics/hipattern.cmi lib/coq/tactics/inv.cmi lib/coq/tactics/leminv.cmi -lib/coq/tactics/rewrite.cmi -lib/coq/tactics/taccoerce.cmi -lib/coq/tactics/tacenv.cmi -lib/coq/tactics/tacintern.cmi -lib/coq/tactics/tacinterp.cmi -lib/coq/tactics/tacsubst.cmi lib/coq/tactics/tactic_matching.cmi -lib/coq/tactics/tactic_option.cmi lib/coq/tactics/tacticals.cmi lib/coq/tactics/tactics.cma lib/coq/tactics/tactics.cmi -lib/coq/tactics/tauto.cmi lib/coq/tactics/term_dnet.cmi lib/coq/theories/Arith/.coq-native/NCoq_Arith_Arith.cmi lib/coq/theories/Arith/.coq-native/NCoq_Arith_Arith.cmo @@ -1052,6 +1052,8 @@ lib/coq/theories/Compat/.coq-native/NCoq lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq84.cmo lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq85.cmi lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq85.cmo +lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq86.cmi +lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq86.cmo lib/coq/theories/Compat/AdmitAxiom.glob lib/coq/theories/Compat/AdmitAxiom.v lib/coq/theories/Compat/AdmitAxiom.vo @@ -1061,6 +1063,9 @@ lib/coq/theories/Compat/Coq84.vo lib/coq/theories/Compat/Coq85.glob lib/coq/theories/Compat/Coq85.v lib/coq/theories/Compat/Coq85.vo +lib/coq/theories/Compat/Coq86.glob +lib/coq/theories/Compat/Coq86.v +lib/coq/theories/Compat/Coq86.vo lib/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.cmi lib/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.cmo lib/coq/theories/FSets/.coq-native/NCoq_FSets_FMapFacts.cmi @@ -1184,6 +1189,8 @@ lib/coq/theories/Init/.coq-native/NCoq_I lib/coq/theories/Init/.coq-native/NCoq_Init_Specif.cmo lib/coq/theories/Init/.coq-native/NCoq_Init_Tactics.cmi lib/coq/theories/Init/.coq-native/NCoq_Init_Tactics.cmo +lib/coq/theories/Init/.coq-native/NCoq_Init_Tauto.cmi +lib/coq/theories/Init/.coq-native/NCoq_Init_Tauto.cmo lib/coq/theories/Init/.coq-native/NCoq_Init_Wf.cmi lib/coq/theories/Init/.coq-native/NCoq_Init_Wf.cmo lib/coq/theories/Init/Datatypes.glob @@ -1213,6 +1220,9 @@ lib/coq/theories/Init/Specif.vo lib/coq/theories/Init/Tactics.glob lib/coq/theories/Init/Tactics.v lib/coq/theories/Init/Tactics.vo +lib/coq/theories/Init/Tauto.glob +lib/coq/theories/Init/Tauto.v +lib/coq/theories/Init/Tauto.vo lib/coq/theories/Init/Wf.glob lib/coq/theories/Init/Wf.v lib/coq/theories/Init/Wf.vo @@ -2054,6 +2064,8 @@ lib/coq/theories/QArith/.coq-native/NCoq lib/coq/theories/QArith/.coq-native/NCoq_QArith_QOrderedType.cmo lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qabs.cmi lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qabs.cmo +lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qcabs.cmi +lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qcabs.cmo lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qcanon.cmi lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qcanon.cmo lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qfield.cmi @@ -2082,6 +2094,9 @@ lib/coq/theories/QArith/QOrderedType.vo lib/coq/theories/QArith/Qabs.glob lib/coq/theories/QArith/Qabs.v lib/coq/theories/QArith/Qabs.vo +lib/coq/theories/QArith/Qcabs.glob +lib/coq/theories/QArith/Qcabs.v +lib/coq/theories/QArith/Qcabs.vo lib/coq/theories/QArith/Qcanon.glob lib/coq/theories/QArith/Qcanon.v lib/coq/theories/QArith/Qcanon.vo @@ -2911,12 +2926,10 @@ lib/coq/theories/ZArith/Zwf.vo lib/coq/theories/ZArith/auxiliary.glob lib/coq/theories/ZArith/auxiliary.v lib/coq/theories/ZArith/auxiliary.vo -lib/coq/tools/compat5.cmo lib/coq/tools/coqdoc/coqdoc.css lib/coq/tools/coqdoc/coqdoc.sty lib/coq/toplevel/assumptions.cmi lib/coq/toplevel/auto_ind_decl.cmi -lib/coq/toplevel/cerrors.cmi lib/coq/toplevel/class.cmi lib/coq/toplevel/classes.cmi lib/coq/toplevel/command.cmi @@ -2924,7 +2937,7 @@ lib/coq/toplevel/coqinit.cmi lib/coq/toplevel/coqloop.cmi lib/coq/toplevel/coqtop.cmi lib/coq/toplevel/discharge.cmi -lib/coq/toplevel/g_obligations.cmi +lib/coq/toplevel/explainErr.cmi lib/coq/toplevel/himsg.cmi lib/coq/toplevel/ind_tables.cmi lib/coq/toplevel/indschemes.cmi
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?201612312305.uBVN59uL045254>