[pkgsrc/trunk]: pkgsrc/lang/coq lang/coq: update to 8.15.2 to make it work wi...

To: pkgsrc-changes-hg%NetBSD.org@localhost
Subject: [pkgsrc/trunk]: pkgsrc/lang/coq lang/coq: update to 8.15.2 to make it work wi...
From: dholland <dholland%pkgsrc.org@localhost>
Date: Tue, 21 Jun 2022 03:13:16 +0000
details:   https://anonhg.NetBSD.org/pkgsrc/rev/dbb00b10fdbc
branches:  trunk
changeset: 380961:dbb00b10fdbc
user:      dholland <dholland%pkgsrc.org@localhost>
date:      Tue Jun 21 02:21:22 2022 +0000

description:
lang/coq: update to 8.15.2 to make it work with current ocaml.

(Update during freeze ok gdt@; even if this version might be broken,
that beats definitely broken.)

pkgsrc changes: use -native-compiler ondemand as recommended upstream.
Now uses dune to build, and uses ocaml-zarith instead of ocaml-num.

Upstream change summary:
(see https://coq.github.io/doc/v8.15/refman/changes.html for the full
change notes)

Coq 8.15.2 fixes:
 - Added: intuition and dintuition use Tauto.intuition_solver (defined
as auto with *) instead of hardcoding auto with *. This makes it
possible to change the default solver with Ltac Tauto.intuition_solver
::= ... (#15866, fixes #7725, by Gaëtan Gilbert).
 - Fixed: uncaught exception UnableToUnify with bidirectionality hints
(#16066, fixes #16063, by Gaëtan Gilbert).
 - Fixed: multiple CoqIDE bugs (#15938, fixes #15861, #15939, fixes
#15882, #15964, fixes #15799, #15984, partially fixes #15873, #15996,
#15912, fixes #15903, all by Jim Fehrle).
 -Fixed: an incorrect implementation of SFClassify, allowing for a
proof of False since 8.11.0, due to Axioms present in
Float.Axioms. (#16101, fixes #16096, by Ali Caglayan).

Coq 8.15.1 fixes:
 - Fixed: cases of incompletenesses in the guard condition for
fixpoints in the presence of cofixpoints or primitive projections
(#15498, fixes #15451, by Hugo Herbelin).
 - Fixed: inconsistency when using module subtyping with squashed
inductives (#15839, fixes #15838 (reported by Pierre-Marie Pédrot), by
Gaëtan Gilbert).
 - Fixed: Check for prior declaration of a custom entry was missing
for notations in only printing mode (#15628, fixes #15619, by Hugo
Herbelin).
 - Fixed: rewrite_strat regression in 8.15.0 related to Transitive
instances (#15577, fixes #15568, by Gaëtan Gilbert).
 - Fixed: When setoid_rewrite succeeds in rewriting at some occurrence
but the resulting equality is the identity, it now tries rewriting in
subterms of that occurrence instead of giving up (#15612, fixes #8080,
by Gaëtan Gilbert).
 - Fixed: Ill-typed goals created by clearbody in the presence of
transitive dependencies in the body of a hypothesis (#15634, fixes
#15606, by Hugo Herbelin).
 - Fixed: cbn knows to refold fixpoints when Arguments with / and !
was used (#15653, fixes #15567, by Gaëtan Gilbert).
 - Fixed a bug where coqc -vok was not creating an empty '.vok'
file. (#15745, by Ramkumar Ramachandra).
 - Fixed: Line numbers shown in the Errors panel of CoqIDE were
incorrect; they didn't match the error locations in the script panel
(#15532, fixes #15531, by Jim Fehrle).
 - Fixed: anomaly when using proof diffs with no focused goal (#15633,
fixes #15578, by Jim Fehrle).
 - Fixed: Attempted edits to the processed part of a buffer while Coq
is busy processing a request are now ignored to ensure "processed"
highlighting is accurate (#15714, fixes #15733 and #15675 and #15725,
by Jim Fehrle).
 - Fixed: Ensure that the names of arguments of inductive schemes are
distinct so that the new Coq 8.15 preservation of argument names in
the with clause of tactics in #13837 works as in Coq 8.14 for these
schemes (#15537, fixes #15420, by Hugo Herbelin).

Coq 8.15.0 summary:
 - The apply with tactic no longer renames arguments unless
compatibility flag Apply With Renaming is set.
 - Improvements to the auto tactic family, fixing the Hint Unfold
behavior, and generalizing the use of discrimination nets.
 - The typeclasses eauto tactic has a new best_effort option allowing
it to return partial solutions to a proof search problem, depending on
the mode declarations associated to each constraint. This mode is used
by typeclass resolution during type inference to provide more precise
error messages.
 - Many commands and options were deprecated or removed after
deprecation and more consistently support locality attributes.
 - The Import command is extended with import_categories to select the
components of a module to import or not, including features such as
hints, coercions, and notations.
 - A visual Ltac debugger is now available in CoqIDE.

Coq 8.14.2 fixes:
 - Instance warns about the default locality immediately rather than
waiting until the instance is ready to be defined. This changes which
command warns when the instance has a separate proof: the Instance
command itself warns instead of the proof closing command (such as
Defined). (#15243, fixes #14704, by Gaëtan Gilbert).

Coq 8.14.1 fixes:
 - Fix the implementation of persistent arrays used by the VM and
native compute so that it uses a uniform representation. Previously,
storing primitive floats inside primitive arrays could cause memory
corruption (#15081, closes #15070, by Pierre-Marie Pédrot).
 - Fixed missing registration of universe constraints in Module Type
elaboration (#14666, fixes #14505, by Hugo Herbelin).
 - Fixed: abstract more robust with respect to Ltac constr bindings
containing existential variables (#14671, fixes #10796, by Hugo
Herbelin).
 - Fixed: correct support of trailing let by tactic specialize
(#15046, fixes #15043, by Hugo Herbelin).
 - Fixed: anomaly with Extraction Conservative Types when extracting
pattern-matching on singleton types (#14669, fixes #3527, by Hugo
Herbelin).
 - Fixed: a regular error instead of an anomaly when calling Separate
Extraction in a module (#14670, fixes #10796, by Hugo Herbelin).

Coq 8.14.0 summary:
 - The internal representation of match has changed to a more space-
efficient and cleaner structure, allowing the fix of a completeness
issue with cumulative inductive types in the type-checker. The
internal representation is now closer to the user-level view of match,
where the argument context of branches and the inductive binders in
and as do not carry type annotations.
 - A new coqnative binary performs separate native compilation of
libraries, starting from a .vo file. It is supported by coq_makefile.
 - Improvements to typeclasses and canonical structure resolution,
allowing more terms to be considered as classes or keys.
 - More control over notations declarations and support for primitive
types in string and number notations.
 - Removal of deprecated tactics, notably omega, which has been
replaced by a greatly improved lia, along with many bug fixes.
 - New Ltac2 APIs for interaction with Ltac1, manipulation of
inductive types and printing.
 - Many changes and additions to the standard library in the numbers,
vectors and lists libraries. A new signed primitive integers library
Sint63 is available in addition to the unsigned Uint63 library.

Coq 8.13.2:
 - Fixed crash when using vm_compute on an irreducible PArray.set
(#14005, fixes #13998, by Guillaume Melquiond).
 - Fix: Never store persistent arrays as VM / native structured
values. This could be used to make vo marshalling crash, and probably
breaking some other invariants of the kernel (#14007, fixes #14006, by
Pierre-Marie Pédrot).
 - Fix: Ltac2 Array.init no longer incurs exponential overhead when
used recursively (#14012, fixes #14011, by Jason Gross).

Coq 8.13.1:
 - Fix arities of VM opcodes for some floating-point operations that
could cause memory corruption (#13867, by Guillaume Melquiond).
 - Added options -v and --version to CoqIDE (#13870, by Guillaume
Melquiond).

Coq 8.13.0 summary:
 - Introduction of primitive persistent arrays in the core language,
implemented using imperative persistent arrays.
 - Introduction of definitional proof irrelevance for the equality
type defined in the SProp sort.
 - Cumulative record and inductive type declarations can now specify
the variance of their universes.
 - Various bugfixes and uniformization of behavior with respect to the
use of implicit arguments and the handling of existential variables in
declarations, unification and tactics.
 - New warning for unused variables in catch-all match branches that
match multiple distinct patterns.
 - New warning for Hint commands outside sections without a locality
attribute, whose goal is to eventually remove the fragile default
behavior of importing hints only when using Require. The recommended
fix is to declare hints as export, instead of the current default
global, meaning that they are imported through Require Import only,
not Require. See the following rationale and guidelines for details.
 - General support for boolean attributes.
 - Many improvements to the handling of notations, including number
notations, recursive notations and notations with bindings. A new
algorithm chooses the most precise notation available to print an
expression, which might introduce changes in printing behavior.
 - Tactic improvements in lia and its zify preprocessing step, now
supporting reasoning on boolean operators such as Z.leb and supporting
primitive integers Int63.
 - Typing flags can now be specified per-constant / inductive.
 - Improvements to the reference manual including updated syntax
descriptions that match Coq's grammar in several chapters, and
splitting parts of the tactics chapter to independent sections.

diffstat:

 lang/coq/MESSAGE                                 |    14 -
 lang/coq/Makefile                                |    32 +-
 lang/coq/PLIST                                   |  6611 ++++++++++-----------
 lang/coq/distinfo                                |    14 +-
 lang/coq/options.mk                              |     3 +-
 lang/coq/patches/patch-Makefile.common           |    17 -
 lang/coq/patches/patch-Makefile.install          |    15 +
 lang/coq/patches/patch-Makefile.make             |     8 +-
 lang/coq/patches/patch-tools_configure_coqide.ml |    17 +
 lang/coq/patches/patch-tools_coqdoc_dune         |    16 +
 10 files changed, 3288 insertions(+), 3459 deletions(-)

diffs (truncated from 7289 to 300 lines):

diff -r 230265ec6727 -r dbb00b10fdbc lang/coq/MESSAGE
--- a/lang/coq/MESSAGE  Tue Jun 21 00:26:04 2022 +0000
+++ /dev/null   Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-===========================================================================
-$NetBSD: MESSAGE,v 1.1.1.1 2003/03/22 20:21:16 kristerw Exp $
-
-You may wish to add the following to your ~/.emacs:
-
-       (add-to-list 'auto-mode-alist '("\\.v$" . coq-mode))
-       (autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t)
-       (autoload 'run-coq "coq-inferior" "Run an inferior Coq process." t)
-       (autoload 'run-coq-other-window "coq-inferior"
-         "Run an inferior Coq process in a new window." t)
-       (autoload 'run-coq-other-frame "coq-inferior"
-         "Run an inferior Coq process in a new frame." t)
-
-===========================================================================
diff -r 230265ec6727 -r dbb00b10fdbc lang/coq/Makefile
--- a/lang/coq/Makefile Tue Jun 21 00:26:04 2022 +0000
+++ b/lang/coq/Makefile Tue Jun 21 02:21:22 2022 +0000
@@ -1,7 +1,6 @@
-# $NetBSD: Makefile,v 1.144 2022/06/03 08:21:55 wiz Exp $
+# $NetBSD: Makefile,v 1.145 2022/06/21 02:21:22 dholland Exp $
 
-DISTNAME=      coq-8.12.2
-PKGREVISION=   4
+DISTNAME=      coq-8.15.2
 CATEGORIES=    lang math
 MASTER_SITES=  ${MASTER_SITE_GITHUB:=coq/}
 GITHUB_TAG=    V${PKGVERSION_NOREV:S/_/+/}
@@ -13,35 +12,30 @@
 
 WRKSRC=                ${WRKDIR}/${GITHUB_PROJECT}-${PKGVERSION_NOREV:S/+/-/}
 
-BROKEN=                "does not support ocaml 4.14"
-
 USE_TOOLS+=            bash
 USE_TOOLS+=            gmake
+OCAML_USE_FINDLIB=     yes
 HAS_CONFIGURE=         yes
 CONFIGURE_ARGS+=       -prefix ${PREFIX}
-#CONFIGURE_ARGS+=      -emacslib ${PREFIX}/share/emacs/site-lisp
 CONFIGURE_ARGS+=       -mandir ${PREFIX}/${PKGMANDIR}
 CONFIGURE_ARGS+=       -configdir ${PKG_SYSCONFDIR}/xdg/coq
 CONFIGURE_ARGS+=       -docdir ${PREFIX}/share/doc/coq
-CONFIGURE_ARGS+=       -coqdocdir ${PREFIX}/share/texmf-dist/tex/latex/coq
-CONFIGURE_ARGS+=       -flambda-opts '-O3 -unbox-closures'
+BUILD_TARGET=          world
 
-BUILDLINK_API_DEPENDS.ocaml+=  ocaml>=3.10
+BUILDLINK_API_DEPENDS.ocaml+=  ocaml>=4.05
 
 # datestamp for reproducible builds (this ends up in compiled proofs)
 # Use the upstream release date plus (arbitrarily) 11 days, the latter
 # being a venture to hopefully avoid accepting compiled proof files from
 # elsewhere that likely are not in fact compatible.
-MAKE_ENV+=             SOURCE_DATE_EPOCH=20201222
+MAKE_ENV+=             SOURCE_DATE_EPOCH=20220611
 
 .include "../../mk/bsd.prefs.mk"
-.include "../../mk/ocaml.mk"
+.include "../../lang/ocaml/ocaml.mk"
 
-PLIST_VARS+=           native
 .if ${OCAML_USE_OPT_COMPILER} == "yes"
 COQIDE_TYPE=           opt
-PLIST.native=          yes
-CONFIGURE_ARGS+=       -native-compiler yes
+CONFIGURE_ARGS+=       -native-compiler ondemand
 UNLIMIT_RESOURCES+=    stacksize # compilation of some files needs this
 BUILD_TARGET=          world
 .else
@@ -82,6 +76,14 @@
 EGDIR=         ${PREFIX}/share/coq/examples
 #CONF_FILES=   {EGDIR}/coqide-gtk2rc ${PKG_SYSCONFDIR}/xdg/coq/coqide-gtk2rc
 
-.include "../../math/ocaml-num/buildlink3.mk"
+# Pull in dune explicitly instead of setting OCAML_USE_DUNE above,
+# because the latter causes pkgsrc to automagically run dune instead
+# of make for the build and that isn't what you're supposed to do.
+.include "../../devel/ocaml-dune/buildlink3.mk"
+
+# Docs say at least 1.10 is required.
+BUILDLINK_API_DEPENDS.ocaml-zarith+=   ocaml-zarith>=1.10
+
+.include "../../math/ocaml-zarith/buildlink3.mk"
 .include "../../mk/pthread.buildlink3.mk"
 .include "../../mk/bsd.pkg.mk"
diff -r 230265ec6727 -r dbb00b10fdbc lang/coq/PLIST
--- a/lang/coq/PLIST    Tue Jun 21 00:26:04 2022 +0000
+++ b/lang/coq/PLIST    Tue Jun 21 02:21:22 2022 +0000
@@ -1,1020 +1,3064 @@
-@comment $NetBSD: PLIST,v 1.31 2021/02/09 22:37:43 dholland Exp $
+@comment $NetBSD: PLIST,v 1.32 2022/06/21 02:21:22 dholland Exp $
 bin/coq-tex
 bin/coq_makefile
 bin/coqc
+bin/coqc.byte
 bin/coqchk
 bin/coqdep
 bin/coqdoc
 ${PLIST.coqide}bin/coqide
-${PLIST.coqide}bin/coqidetop
+${PLIST.coqide}bin/coqidetop.byte
 ${PLIST.coqide}bin/coqidetop.opt
+bin/coqnative
 bin/coqpp
 bin/coqproofworker.opt
 bin/coqqueryworker.opt
 bin/coqtacticworker.opt
 bin/coqtop
+bin/coqtop.byte
 bin/coqtop.opt
 bin/coqwc
 bin/coqworkmgr
+bin/csdpcert
 bin/ocamllibdep
 bin/votour
-lib/coq/META
-lib/coq/clib/bigint.cmi
-${PLIST.ocaml-opt}lib/coq/clib/bigint.cmx
-lib/coq/clib/cArray.cmi
-${PLIST.ocaml-opt}lib/coq/clib/cArray.cmx
-lib/coq/clib/cEphemeron.cmi
-${PLIST.ocaml-opt}lib/coq/clib/cEphemeron.cmx
-lib/coq/clib/cList.cmi
-${PLIST.ocaml-opt}lib/coq/clib/cList.cmx
-lib/coq/clib/cMap.cmi
-${PLIST.ocaml-opt}lib/coq/clib/cMap.cmx
-lib/coq/clib/cObj.cmi
-${PLIST.ocaml-opt}lib/coq/clib/cObj.cmx
-lib/coq/clib/cSet.cmi
-${PLIST.ocaml-opt}lib/coq/clib/cSet.cmx
-lib/coq/clib/cSig.cmi
-lib/coq/clib/cString.cmi
-${PLIST.ocaml-opt}lib/coq/clib/cString.cmx
-lib/coq/clib/cThread.cmi
-${PLIST.ocaml-opt}lib/coq/clib/cThread.cmx
-lib/coq/clib/cUnix.cmi
-${PLIST.ocaml-opt}lib/coq/clib/cUnix.cmx
-${PLIST.ocaml-opt}lib/coq/clib/clib.a
-${PLIST.ocaml-opt}lib/coq/clib/clib.cmxa
-lib/coq/clib/diff2.cmi
-${PLIST.ocaml-opt}lib/coq/clib/diff2.cmx
-lib/coq/clib/dyn.cmi
-${PLIST.ocaml-opt}lib/coq/clib/dyn.cmx
-lib/coq/clib/exninfo.cmi
-${PLIST.ocaml-opt}lib/coq/clib/exninfo.cmx
-lib/coq/clib/hMap.cmi
-${PLIST.ocaml-opt}lib/coq/clib/hMap.cmx
-lib/coq/clib/hashcons.cmi
-${PLIST.ocaml-opt}lib/coq/clib/hashcons.cmx
-lib/coq/clib/hashset.cmi
-${PLIST.ocaml-opt}lib/coq/clib/hashset.cmx
-lib/coq/clib/heap.cmi
-${PLIST.ocaml-opt}lib/coq/clib/heap.cmx
-lib/coq/clib/iStream.cmi
-${PLIST.ocaml-opt}lib/coq/clib/iStream.cmx
-lib/coq/clib/int.cmi
-${PLIST.ocaml-opt}lib/coq/clib/int.cmx
-lib/coq/clib/minisys.cmi
-${PLIST.ocaml-opt}lib/coq/clib/minisys.cmx
-lib/coq/clib/monad.cmi
-${PLIST.ocaml-opt}lib/coq/clib/monad.cmx
-lib/coq/clib/option.cmi
-${PLIST.ocaml-opt}lib/coq/clib/option.cmx
-lib/coq/clib/orderedType.cmi
-${PLIST.ocaml-opt}lib/coq/clib/orderedType.cmx
-lib/coq/clib/predicate.cmi
-${PLIST.ocaml-opt}lib/coq/clib/predicate.cmx
-lib/coq/clib/range.cmi
-${PLIST.ocaml-opt}lib/coq/clib/range.cmx
-lib/coq/clib/segmenttree.cmi
-${PLIST.ocaml-opt}lib/coq/clib/segmenttree.cmx
-lib/coq/clib/store.cmi
-${PLIST.ocaml-opt}lib/coq/clib/store.cmx
-lib/coq/clib/terminal.cmi
-${PLIST.ocaml-opt}lib/coq/clib/terminal.cmx
-lib/coq/clib/trie.cmi
-${PLIST.ocaml-opt}lib/coq/clib/trie.cmx
-lib/coq/clib/unicode.cmi
-${PLIST.ocaml-opt}lib/coq/clib/unicode.cmx
-lib/coq/clib/unicodetable.cmi
-${PLIST.ocaml-opt}lib/coq/clib/unicodetable.cmx
-lib/coq/clib/unionfind.cmi
-${PLIST.ocaml-opt}lib/coq/clib/unionfind.cmx
-${PLIST.ocaml-opt}lib/coq/config/config.a
-${PLIST.ocaml-opt}lib/coq/config/config.cmxa
-lib/coq/config/coq_config.cmi
-${PLIST.ocaml-opt}lib/coq/config/coq_config.cmx
-lib/coq/coqpp/coqpp_ast.cmi
-lib/coq/coqpp/coqpp_parse.cmi
-lib/coq/coqpp/coqpp_parser.cmi
-lib/coq/engine/eConstr.cmi
-${PLIST.ocaml-opt}lib/coq/engine/eConstr.cmx
-${PLIST.ocaml-opt}lib/coq/engine/engine.a
-${PLIST.ocaml-opt}lib/coq/engine/engine.cmxa
-lib/coq/engine/evar_kinds.cmi
-${PLIST.ocaml-opt}lib/coq/engine/evar_kinds.cmx
-lib/coq/engine/evarutil.cmi
-${PLIST.ocaml-opt}lib/coq/engine/evarutil.cmx
-lib/coq/engine/evd.cmi
-${PLIST.ocaml-opt}lib/coq/engine/evd.cmx
-lib/coq/engine/ftactic.cmi
-${PLIST.ocaml-opt}lib/coq/engine/ftactic.cmx
-lib/coq/engine/logic_monad.cmi
-${PLIST.ocaml-opt}lib/coq/engine/logic_monad.cmx
-lib/coq/engine/namegen.cmi
-${PLIST.ocaml-opt}lib/coq/engine/namegen.cmx
-lib/coq/engine/nameops.cmi
-${PLIST.ocaml-opt}lib/coq/engine/nameops.cmx
-lib/coq/engine/proofview.cmi
-${PLIST.ocaml-opt}lib/coq/engine/proofview.cmx
-lib/coq/engine/proofview_monad.cmi
-${PLIST.ocaml-opt}lib/coq/engine/proofview_monad.cmx
-lib/coq/engine/termops.cmi
-${PLIST.ocaml-opt}lib/coq/engine/termops.cmx
-lib/coq/engine/uState.cmi
-${PLIST.ocaml-opt}lib/coq/engine/uState.cmx
-lib/coq/engine/univGen.cmi
-${PLIST.ocaml-opt}lib/coq/engine/univGen.cmx
-lib/coq/engine/univMinim.cmi
-${PLIST.ocaml-opt}lib/coq/engine/univMinim.cmx
-lib/coq/engine/univNames.cmi
-${PLIST.ocaml-opt}lib/coq/engine/univNames.cmx
-lib/coq/engine/univProblem.cmi
-${PLIST.ocaml-opt}lib/coq/engine/univProblem.cmx
-lib/coq/engine/univSubst.cmi
-${PLIST.ocaml-opt}lib/coq/engine/univSubst.cmx
-lib/coq/engine/univops.cmi
-${PLIST.ocaml-opt}lib/coq/engine/univops.cmx
-${PLIST.ocaml-opt}lib/coq/gramlib/.pack/gramlib.a
-lib/coq/gramlib/.pack/gramlib.cmi
-${PLIST.ocaml-opt}lib/coq/gramlib/.pack/gramlib.cmx
-${PLIST.ocaml-opt}lib/coq/gramlib/.pack/gramlib.cmxa
-lib/coq/gramlib/.pack/gramlib__Gramext.cmi
-${PLIST.ocaml-opt}lib/coq/gramlib/.pack/gramlib__Gramext.cmx
-lib/coq/gramlib/.pack/gramlib__Grammar.cmi
-${PLIST.ocaml-opt}lib/coq/gramlib/.pack/gramlib__Grammar.cmx
-lib/coq/gramlib/.pack/gramlib__Plexing.cmi
-${PLIST.ocaml-opt}lib/coq/gramlib/.pack/gramlib__Plexing.cmx
-lib/coq/gramlib/.pack/gramlib__Ploc.cmi
-${PLIST.ocaml-opt}lib/coq/gramlib/.pack/gramlib__Ploc.cmx
-${PLIST.coqide}lib/coq/ide/config_lexer.cmi
-${PLIST.coqide}lib/coq/ide/configwin.cmi
-${PLIST.coqide}lib/coq/ide/configwin_ihm.cmi
-${PLIST.coqide}lib/coq/ide/configwin_messages.cmi
-${PLIST.coqide}lib/coq/ide/coq.cmi
-${PLIST.coqide}lib/coq/ide/coqOps.cmi
-${PLIST.coqide}lib/coq/ide/coq_commands.cmi
-${PLIST.coqide}lib/coq/ide/coq_lex.cmi
-${PLIST.coqide}lib/coq/ide/coqide.cmi
-${PLIST.coqide}lib/coq/ide/coqide_ui.cmi
-${PLIST.coqide}lib/coq/ide/document.cmi
-${PLIST.coqide}lib/coq/ide/fileOps.cmi
-${PLIST.coqide}lib/coq/ide/gtk_parsing.cmi
-${PLIST.ocaml-opt}${PLIST.coqide}lib/coq/ide/ide.a
-${PLIST.ocaml-opt}${PLIST.coqide}lib/coq/ide/ide.cmxa
-${PLIST.coqide}lib/coq/ide/ideutils.cmi
-${PLIST.coqide}lib/coq/ide/microPG.cmi
-${PLIST.coqide}lib/coq/ide/minilib.cmi
-${PLIST.coqide}lib/coq/ide/preferences.cmi
-${PLIST.coqide}lib/coq/ide/sentence.cmi
-${PLIST.coqide}lib/coq/ide/session.cmi
-${PLIST.coqide}lib/coq/ide/tags.cmi
-${PLIST.coqide}lib/coq/ide/unicode_bindings.cmi
-${PLIST.coqide}lib/coq/ide/utf8_convert.cmi
-${PLIST.coqide}lib/coq/ide/wg_Command.cmi
-${PLIST.coqide}lib/coq/ide/wg_Completion.cmi
-${PLIST.coqide}lib/coq/ide/wg_Detachable.cmi
-${PLIST.coqide}lib/coq/ide/wg_Find.cmi
-${PLIST.coqide}lib/coq/ide/wg_MessageView.cmi
-${PLIST.coqide}lib/coq/ide/wg_Notebook.cmi
-${PLIST.coqide}lib/coq/ide/wg_ProofView.cmi
-${PLIST.coqide}lib/coq/ide/wg_RoutedMessageViews.cmi
-${PLIST.coqide}lib/coq/ide/wg_ScriptView.cmi
-${PLIST.coqide}lib/coq/ide/wg_Segment.cmi
-lib/coq/interp/constrexpr.cmi
-${PLIST.ocaml-opt}lib/coq/interp/constrexpr.cmx
-lib/coq/interp/constrexpr_ops.cmi
-${PLIST.ocaml-opt}lib/coq/interp/constrexpr_ops.cmx
-lib/coq/interp/constrextern.cmi
-${PLIST.ocaml-opt}lib/coq/interp/constrextern.cmx
-lib/coq/interp/constrintern.cmi
-${PLIST.ocaml-opt}lib/coq/interp/constrintern.cmx
-lib/coq/interp/decls.cmi
-${PLIST.ocaml-opt}lib/coq/interp/decls.cmx
-lib/coq/interp/deprecation.cmi
-${PLIST.ocaml-opt}lib/coq/interp/deprecation.cmx
-lib/coq/interp/dumpglob.cmi
-${PLIST.ocaml-opt}lib/coq/interp/dumpglob.cmx
-lib/coq/interp/genintern.cmi
-${PLIST.ocaml-opt}lib/coq/interp/genintern.cmx
-lib/coq/interp/impargs.cmi
-${PLIST.ocaml-opt}lib/coq/interp/impargs.cmx
-lib/coq/interp/implicit_quantifiers.cmi
-${PLIST.ocaml-opt}lib/coq/interp/implicit_quantifiers.cmx
-${PLIST.ocaml-opt}lib/coq/interp/interp.a
-${PLIST.ocaml-opt}lib/coq/interp/interp.cmxa
Prev by Date: [pkgsrc/trunk]: pkgsrc/doc CHANGES for lang/coq
Next by Date: [pkgsrc/trunk]: pkgsrc/doc TODO: I have a partial update for camlp5, doesn't ...
Previous by Thread: [pkgsrc/trunk]: pkgsrc/doc CHANGES for lang/coq
Next by Thread: [pkgsrc/trunk]: pkgsrc/doc TODO: I have a partial update for camlp5, doesn't ...
Indexes:
Home | Main Index | Thread Index | Old Index