---
- branch: MAIN
  date: Mon Oct 29 11:33:18 UTC 2012
  files:
  - new: '1.51'
    old: '1.50'
    path: pkgsrc/lang/coq/Makefile
    pathrev: pkgsrc/lang/coq/Makefile@1.51
    type: modified
  - new: '1.12'
    old: '1.11'
    path: pkgsrc/lang/coq/PLIST
    pathrev: pkgsrc/lang/coq/PLIST@1.12
    type: modified
  - new: '0'
    old: '1.1'
    path: pkgsrc/lang/coq/PLIST.natdynlink
    pathrev: pkgsrc/lang/coq/PLIST.natdynlink@0
    type: deleted
  - new: '0'
    old: '1.7'
    path: pkgsrc/lang/coq/PLIST.opt
    pathrev: pkgsrc/lang/coq/PLIST.opt@0
    type: deleted
  - new: '1.14'
    old: '1.13'
    path: pkgsrc/lang/coq/distinfo
    pathrev: pkgsrc/lang/coq/distinfo@1.14
    type: modified
  - new: '1.1'
    old: '0'
    path: pkgsrc/lang/coq/patches/patch-Makefile.build
    pathrev: pkgsrc/lang/coq/patches/patch-Makefile.build@1.1
    type: added
  - new: '1.1'
    old: '0'
    path: pkgsrc/lang/coq/patches/patch-ide_preferences.ml
    pathrev: pkgsrc/lang/coq/patches/patch-ide_preferences.ml@1.1
    type: added
  - new: '1.1'
    old: '0'
    path: pkgsrc/lang/coq/patches/patch-ide_utils_okey.ml
    pathrev: pkgsrc/lang/coq/patches/patch-ide_utils_okey.ml@1.1
    type: added
  - new: '0'
    old: '1.2'
    path: pkgsrc/lang/coq/patches/patch-ac
    pathrev: pkgsrc/lang/coq/patches/patch-ac@0
    type: deleted
  id: 20121029T113318Z.4c5f9c1d16b8dae5557c2e432f886daf3c2b7fea
  log: "Taken over maintainership (as discussed with previous maintainer,\nrichards@cs.princeton.edu).
    Updated package to use PLIST_VARS and CONF_FILES.\nUpdated coq to version 8.4.
    Changes include:\n\nLogic\n- Standard eta-conversion now supported (dependent
    product only).\n- Guard condition improvement: subterm property is propagated
    through beta-redex\n  blocked by pattern-matching, as in \"(match v with C ..
    => fun x => u end) x\";\n  this allows for instance to use \"rewrite ... in ...\"
    without breaking\n  the guard condition.\nVernacular commands\n- The \"Reset\"
    command is now supported again in files given to coqc or Load.\n- \"Show Script\"
    now indents again the displayed scripts. It can also work\n  correctly across
    Load'ed files if the option \"Unset Atomic Load\" is used.\n- \"Open Scope\" can
    now be given the delimiter (e.g. Z) instead of the full\n  scope name (e.g. Z_scope).\n-
    Commands \"Back\" and \"BackTo\" are now handling the proof states. They may\n
    \ perform some extra steps of backtrack to avoid states where the proof\n  state
    is unavailable (typically a closed proof).\n- The commands \"Suspend\" and \"Resume\"
    have been removed.\n- A basic Show Script has been reintroduced (no indentation).\n-
    New command \"Set Parsing Explicit\" for deactivating parsing (and printing)\n
    \ of implicit arguments (useful for teaching).\n- New command \"Grab Existential
    Variables\" to transform the unresolved evars\n  at the end of a proof into goals.\n-
    It is now mandatory to have a space (or tabulation or newline or end-of-file)\n
    \ after a \".\" ending a sentence.\n- In SearchAbout, the [ ] delimiters are now
    optional.\n- New command \"Add/Remove Search Blacklist <substring> ...\":\n  a
    Search or SearchAbout or similar query will never mention lemmas\n  whose qualified
    names contain any of the declared substrings.\n  The default blacklisted substrings
    are \"_admitted\" \"_subproof\" \"Private_\".\n- When the output file of \"Print
    Universes\" ends in \".dot\" or \".gv\",\n  the universe graph is printed in the
    DOT language, and can be\n  processed by Graphviz tools.\n- New command \"Print
    Sorted Universes\".\n- The undocumented and obsolete option \"Set/Unset Boxed
    Definitions\" has\n  been removed, as well as syntaxes like \"Boxed Fixpoint foo\".\n-
    A new option \"Set Default Timeout n / Unset Default Timeout\".\n- Qed now uses
    information from the reduction tactics used in proof script\n  to avoid conversion
    at Qed time to go into a very long computation.\n- New command \"Show Goal ident\"
    to display the statement of a goal, even\n  a closed one (available from Proof
    General).\n- Command \"Proof\" accept a new modifier \"using\" to force generalization\n
    \ over a given list of section variables at section ending.\n- New command \"Arguments\"
    generalizing \"Implicit Arguments\" and\n  \"Arguments Scope\" and that also allows
    to rename the parameters of a\n  definition and to tune the behavior of the tactic
    \"simpl\".\nSpecification language and Notations\n- Most compatibility notations
    of the standard library are now tagged as\n  (compat xyz), where xyz is a former
    Coq version, for instance \"8.3\".\n  These notations behave as (only parsing)
    notations, except that they may\n  triggers warnings (or errors) when used while
    Coq is not in a corresponding\n  -compat mode.\n- To activate these compatibility
    warnings, use \"Set Verbose Compat Notations\"\n  or the command-line flag -verbose-compat-notations.\n-
    For a strict mode without these compatibility notations, use\n  \"Unset Compat
    Notations\" or the command-line flag -no-compat-notations.\n- Maximal implicit
    arguments can now be set locally by { }. The registration\n  traverses fixpoints
    and lambdas. Because there is conversion in types,\n  maximal implicit arguments
    are not taken into account in partial\n  applications (use eta expanded form with
    explicit { } instead).\n- Added support for recursive notations with binders (allows
    for instance\n  to write \"exists x y z, P\").\n- Structure/Record printing can
    be disable by \"Unset Printing Records\".\n  In addition, it can be controlled
    on type by type basis using\n  \"Add Printing Record\" or \"Add Printing Constructor\".\n-
    Pattern-matching compilation algorithm: in \"match x, y with ... end\",\n  possible
    dependencies of x (or of the indices of its type) in the type\n  of y are now
    taken into account.\nTactics\n- An annotation \"eqn:H\" or \"eqn:?\" can be added
    to a \"destruct\"\n  or \"induction\" to make it generate equations in the spirit
    of \"case_eq\".\n  The former syntax \"_eqn\" is discontinued.\n- The name of
    the hypothesis introduced by tactic \"remember\" can be\n  set via the new syntax
    \"remember t as x eqn:H\" (wish #2489).\n- Still no general \"info\" tactical,
    but new specific tactics info_auto,\n  info_eauto, info_trivial which provides
    information on the proofs found\n  by auto/eauto/trivial. Display of these details
    could also be activated by\n  \"Set Info Auto\"/\"Set Info Eauto\"/\"Set Info
    Trivial\".\n- Details on everything tried by auto/eauto/trivial during a proof
    search\n  could be obtained by \"debug auto\", \"debug eauto\", \"debug trivial\"
    or by a\n  global \"Set Debug Auto\"/\"Set Debug Eauto\"/\"Set Debug Trivial\".\n-
    New command \"r string\" in Ltac debugger that interprets \"idtac\n  string\"
    in Ltac code as a breakpoint and jumps to its next use.\n- Tactics from the Dp
    plugin (simplify, ergo, yices, cvc3, z3, cvcl,\n  harvey, zenon, gwhy) have been
    removed, since Why2 has not been\n  maintained for the last few years. The Why3
    plugin should be a suitable\n  replacement in most cases.\n- New proof engine.\n-
    Scripts can now be structured thanks to bullets - * + and to subgoal\n  delimitation
    via { }. Note: for use with Proof General, a cvs version of\n  Proof General no
    older than mid-July 2011 is currently required.\n- Support for tactical \"info\"
    is suspended.\n- Support for command \"Show Script\" is suspended.\n- New tactics
    constr_eq, is_evar and has_evar for use in Ltac.\n- Removed the two-argument variant
    of \"decide equality\".\n- New experimental tactical \"timeout <n> <tac>\". Since
    <n> is a time\n  in second for the moment, this feature should rather be avoided\n
    \ in scripts meant to be machine-independent.\n- Fix in \"destruct\": removal
    of unexpected local definitions in context might\n  result in some rare incompatibilities
    (solvable by adapting name hypotheses).\n- Introduction pattern \"_\" made more
    robust.\n- Tactic (and Eval command) vm_compute can now be interrupted via Ctrl-C.\n-
    Unification in \"apply\" supports unification of patterns of the form\n  ?f x
    y = g(x,y) (compatibility ensured by using\n  \"Unset Tactic Pattern Unification\").
    It also supports (full) betaiota.\n- Tactic autorewrite does no longer instantiate
    pre-existing\n  existential variables (theoretical source of possible incompatibilities).\n-
    Tactic \"dependent rewrite\" now supports equality in \"sig\".\n- Tactic omega
    now understands Zpred (wish #1912) and can prove any goal\n  from a context containing
    an arithmetical contradiction (wish #2236).\n- Using \"auto with nocore\" disables
    the use of the \"core\" database (wish #2188).\n  This pseudo-database \"nocore\"
    can also be used with trivial and eauto.\n- Tactics \"set\", \"destruct\" and
    \"induction\" accepts incomplete terms and\n  use the goal to complete the pattern
    assuming it is non ambiguous.\n- When used on arguments with a dependent type,
    tactics such as\n  \"destruct\", \"induction\", \"case\", \"elim\", etc. now try
    to abstract\n  automatically the dependencies over the arguments of the types\n
    \ (based on initial ideas from Chung-Kil Hur, extension to nested\n   dependencies
    suggested by Dan Grayson)\n- Tactic \"injection\" now failing on an equality showing
    no constructors while\n  it was formerly generalizing again the goal over the
    given equality.\n- In Ltac, the \"context [...]\" syntax has now a variant \"appcontext
    [...]\"\n  allowing to match partial applications in larger applications.\n- When
    applying destruct or inversion on a fixpoint hiding an inductive\n  type, recursive
    calls to the fixpoint now remain folded by default (rare\n  source of incompatibility
    generally solvable by adding a call to simpl).\n- In an ltac pattern containing
    a \"match\", a final \"| _ => _\" branch could be\n  used now instead of enumerating
    all remaining constructors. Moreover, the\n  pattern \"match _ with _ => _ end\"
    now allows to match any \"match\". A \"in\"\n  annotation can also be added to
    restrict to a precise inductive type.\n- The behavior of \"simpl\" can be tuned
    using the \"Arguments\" vernacular.\n  In particular constants can be marked so
    that they are always/never unfolded\n  by \"simpl\", or unfolded only when a set
    of arguments evaluates to a\n  constructor. Last one can mark a constant so that
    it is unfolded only if the\n  simplified term does not expose a match in head
    position.\nLibraries\n- Reals: changed definition of PI, no more axiom about sin(PI/2).\n-
    SetoidPermutation: a notion of permutation for lists modulo a setoid equality.\n-
    BigN: fixed the ocaml code doing the parsing/printing of big numbers.\n- MSetRBT:
    a new implementation of MSets via Red-Black trees (initial\n  contribution by
    Andrew Appel).\n- MSetAVL: for maximal sharing with the new MSetRBT, the argument
    order\n  of Node has changed (this should be transparent to regular MSets users).\n-
    Extension of the abstract part of Numbers, which now provide axiomatizations\n
    \ and results about many more integer functions, such as pow, gcd, lcm, sqrt,\n
    \ log2 and bitwise functions. These functions are implemented for nat, N, BigN,\n
    \ Z, BigZ. See in particular file NPeano for new functions about nat.\n- The definition
    of types positive, N, Z is now in file BinNums.v\n- Major reorganization of ZArith.
    The initial file ZArith/BinInt.v now contains\n  an internal module Z implementing
    the Numbers interface for integers.\n  This module Z regroups:\n  * all functions
    over type Z : Z.add, Z.mul, ...\n  * the minimal proofs of specifications for
    these functions : Z.add_0_l, ...\n  * an instantation of all derived properties
    proved generically in Numbers :\n    Z.add_comm, Z.add_assoc, ...\n  A large part
    of ZArith is now simply compatibility notations, for instance\n  Zplus_comm is
    an alias for Z.add_comm. The direct use of module Z is now\n  recommended instead
    of relying on these compatibility notations.\n- Similar major reorganization of
    NArith, via a module N in NArith/BinNat.v\n- Concerning the positive datatype,
    BinPos.v is now in a specific directory\n  PArith, and contains an internal submodule
    Pos. We regroup there functions\n  such as Pos.add Pos.mul etc as well as many
    results about them. These results\n  are here proved directly (no Number interface
    for strictly positive numbers).\n- Note that in spite of the compatibility layers,
    all these reorganizations\n  may induce some marginal incompatibilies in scripts.
    In particular:\n  * the \"?=\" notation for positive now refers to a binary function
    Pos.compare,\n    instead of the infamous ternary Pcompare (now Pos.compare_cont).\n
    \ * some hypothesis names generated by the system may changed (typically for\n
    \   a \"destruct Z_le_gt_dec\") since naming is done after the short name of\n
    \   the head predicate (here now \"le\" in module Z instead of \"Zle\", etc).\n
    \ * the internals of Z.add has changed, now relying of Z.pos_sub.\n- Also note
    these new notations:\n  * \"<?\" \"<=?\" \"=?\" for boolean tests such as Z.ltb
    Z.leb Z.eqb.\n  * \"æ­\x8E\" for the alternative integer division Z.quot implementing
    the Truncate\n    convention (former ZOdiv), while the notation for the Coq usual
    division\n    Z.div implementing the Flooring convention remains \"/\". Their
    corresponding\n    modulo functions are Z.rem (no notations) for Z.quot and Z.modulo
    (infix\n    \"mod\" notation) for Z.div.\n- Lemmas about conversions between these
    datatypes are also organized\n  in modules, see for instance modules Z2Nat, N2Z,
    etc.\n- When creating BigN, the macro-generated part NMake_gen is much smaller.\n
    \ The generic part NMake has been reworked and improved. Some changes\n  may introduce
    incompatibilities. In particular, the order of the arguments\n  for BigN.shiftl
    and BigN.shiftr is now reversed: the number to shift now\n  comes first. By default,
    the power function now takes two BigN.\n- Creation of Vector, an independent library
    for lists indexed by their length.\n  Vectors' names overwrite lists' one so you
    should not \"Import\" the library.\n  All old names changed: function names follow
    the ocaml ones and, for example,\n  Vcons becomes Vector.cons. You can get [..;..;..]-style
    notations by importing\n  Vector.VectorNotations.\n- Removal of TheoryList. Requiring
    List instead should work most of the time.\n- New syntax \"rew Heq in H\" and
    \"rew <- Heq in H\" for eq_rect and\n  eq_rect_r (available by importing module
    EqNotations).\n- Wf.iter_nat is now Peano.nat_iter (with an implicit type argument).\nModule
    System\n- The names of modules (and module types) are now in a fully separated\n
    \ namespace from ordinary definitions: \"Definition E:=0. Module E. End E.\"\n
    \ is now accepted.\n- During subtyping checks, an opaque constant in a module
    type could now\n  be implemented by anything of the right type, even if bodies
    differ.\n  Said otherwise, with respect to subtyping, an opaque constant behaves\n
    \ just as a parameter. Coqchk was already implementing this, but not coqtop.\n-
    The inlining done during application of functors can now be controlled\n  more
    precisely, by the annotations (no inline) or (inline at level XX).\n  With the
    latter annotation, only functor parameters whose levels\n  are lower or equal
    than XX will be inlined.\n  The level of a parameter can be fixed by \"Parameter
    Inline(30) foo\".\n  When levels aren't given, the default value is 100. One can
    also use\n  the flag \"Set Inline Level ...\" to set a level.\n- Print Assumptions
    should now handle correctly opaque modules (#2168).\n- Print Module (Type) now
    tries to print more details, such as types and\n  bodies of the module elements.
    Note that Print Module Type could be\n  used on a module to display only its interface.
    The option\n  \"Set Short Module Printing\" could be used to switch back to the
    earlier\n  behavior were only field names were displayed.\nCoqIDE\n- Coqide now
    supports the \"Restart\" command, and \"Undo\" (with a warning).\n  Better support
    for \"Abort\".\n- Coqide now runs coqtop as separated process, making it more
    robust:\n  coqtop subprocess can be interrupted, or even killed and relaunched\n
    \ (cf button \"Restart Coq\", ex-\"Go to Start\"). For allowing such\n  interrupts,
    the Windows version of coqide now requires Windows >= XP\n  SP1.\n- The communication
    between CoqIDE and Coqtop is now done via a dialect of XML.\n- The backtrack engine
    of CoqIDE has been reworked, it now uses the\n  \"Backtrack\" command similarly
    to Proof General.\n- The Coqide parsing of sentences has be reworked and now supports\n
    \ tactic delimitation via { }.\n- Coqide now accepts the Abort command (wish #2357).\n-
    Coqide can read coq_makefile files as \"project file\" and use it to\n  set automatically
    options to send to coqtop.\n- Preference files have moved to $XDG_CONFIG_HOME/coq
    and accelerators\n  are not stored as a list anymore.\nInternal infrastructure\n-
    Opaque proofs are now loaded lazily by default. This allows to be almost as\n
    \ fast as -dont-load-proofs, while being safer (no creation of axioms) and\n  avoiding
    feature restrictions (Print and Print Assumptions work ok).\n- Revised hash-consing
    code allowing more sharing of memory\n- Experimental support added for camlp4
    (the one provided alongside ocaml),\n  simply pass option -usecamlp4 to ./configure.
    By default camlp5 is used.\n- Revised build system: no more stages in Makefile
    thanks to some recursive\n  aspect of recent gnu make, use of vo.itarget files
    containing .v to compile\n  for both make and ocamlbuild, etc.\n- Support of cross-compilation
    via mingw from unix toward Windows,\n  contact P. Letouzey for more informations.\n-
    New Makefile rules mli-doc to make html of mli in dev/doc/html and\n  full-stdlib
    to get a (huge) pdf reflecting the whole standard library.\nExtraction\n- By default,
    opaque terms are now truly considered opaque by extraction:\n  instead of accessing
    their body, they are now considered as axioms.\n  The previous behaviour can be
    reactivated via the option\n  \"Set Extraction AccessOpaque\".\n- The pretty-printer
    for Haskell now produces layout-independant code\n- A new command \"Separate Extraction
    cst1 cst2 ...\" that mixes a\n  minimal extracted environment a la \"Recursive
    Extraction\" and the\n  production of several files (one per coq source) a la
    \"Extraction Library\".\n- New option \"Set/Unset Extraction KeepSingleton\" for
    preventing the\n  extraction to optimize singleton container types.\n- The extraction
    now identifies and properly rejects a particular case of\n  universe polymorphism
    it cannot handle yet (the pair (I,I) being Prop).\n- Support of anonymous fields
    in record (#2555).\nTools\n- Coq now searches directories specified in COQPATH,
    $XDG_DATA_HOME/coq,\n  $XDG_DATA_DIRS/coq, and user-contribs before the standard
    library.\n- Coq rc file has moved to $XDG_CONFIG_HOME/coq.\n- Major changes to
    coq_makefile:\n  * mli/mlpack/mllib taken into account, ml not preproccessed anymore,
    ml4 work;\n  * mlihtml generates doc of mli, install-doc install the html doc
    in DOCDIR\n    with the same policy as vo in COQLIB;\n  * More variables are given
    by coqtop -config, others are defined only if the\n    users doesn't have defined
    them elsewhere. Consequently, generated makefile\n    should work directly on
    any architecture;\n  * Packagers can take advantage of $(DSTROOT) introduction.
    Installation can\n    be made in $XDG_DATA_HOME/coq;\n  * -arg option allows to
    send option as argument to coqc.\n"
  module: pkgsrc
  subject: 'CVS commit: pkgsrc/lang/coq'
  unixtime: '1351510398'
  user: jaapb