The NetBSD Project

CVS log for pkgsrc/lang/coq/PLIST

[BACK] Up to [] / pkgsrc / lang / coq

Request diff between arbitrary revisions

Default branch: MAIN

Revision 1.32 / (download) - annotate - [select for diffs], Tue Jun 21 02:21:22 2022 UTC (17 months, 2 weeks ago) by dholland
Branch: MAIN
CVS Tags: pkgsrc-2023Q3-base, pkgsrc-2023Q3, pkgsrc-2023Q2-base, pkgsrc-2023Q2, pkgsrc-2023Q1-base, pkgsrc-2023Q1, pkgsrc-2022Q4-base, pkgsrc-2022Q4, pkgsrc-2022Q3-base, pkgsrc-2022Q3, pkgsrc-2022Q2-base, pkgsrc-2022Q2, HEAD
Changes since 1.31: +3209 -3402 lines
Diff to previous 1.31 (colored)

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 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
 - 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
 - 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
 - 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

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.

Revision 1.31 / (download) - annotate - [select for diffs], Tue Feb 9 22:37:43 2021 UTC (2 years, 9 months ago) by dholland
Branch: MAIN
CVS Tags: pkgsrc-2022Q1-base, pkgsrc-2022Q1, pkgsrc-2021Q4-base, pkgsrc-2021Q4, pkgsrc-2021Q3-base, pkgsrc-2021Q3, pkgsrc-2021Q2-base, pkgsrc-2021Q2, pkgsrc-2021Q1-base, pkgsrc-2021Q1
Changes since 1.30: +1962 -694 lines
Diff to previous 1.30 (colored)

Update lang/coq to 8.12.2.

Fixes build with current ocaml.

Note: this update includes the import semantics fixes from 8.11 that
break a lot of developments.

pkgsrc change: docs build now works.

Summary of changes in 8.12:

Coq version 8.12 integrates many usability improvements, in particular
with respect to notations, scopes and implicit arguments, along with
many bug fixes and major improvements to the reference manual. The
main changes include:

    New binder notation for non-maximal implicit arguments using [ ]
    allowing to set and see the implicit status of arguments

    New notation Inductive I A | x : s := ... to distinguish the
    uniform from the non-uniform parameters in inductive definitions.

    More robust and expressive treatment of implicit inductive
    parameters in inductive declarations.

    Improvements in the treatment of implicit arguments and partially
    applied constants in notations, parsing of hexadecimal number
    notation and better handling of scopes and coercions for printing.

    A correct and efficient coercion coherence checking algorithm,
    avoiding spurious or duplicate warnings.

    An improved Search command which accepts complex queries. Note
    that this takes precedence over the now deprecated ssreflect

    Many additions and improvements of the standard library.

    Improvements to the reference manual include a more logical
    organization of chapters along with updated syntax descriptions
    that match Coq's grammar in most but not all chapters.

Additionally, the omega tactic is deprecated in this version of Coq,
and we recommend users to switch to lia in new proof scripts (see also
the warning message in the corresponding chapter).

Summary of changes in 8.11:

The main changes brought by Coq version 8.11 are:

    Ltac2, a new tactic language for writing more robust larger scale
    tactics, with built-in support for datatypes and the multi-goal
    tactic monad.

    Primitive floats are integrated in terms and follow the binary64
    format of the IEEE 754 standard, as specified in the
    Coq.Float.Floats library.

    Cleanups of the section mechanism, delayed proofs and further
    restrictions of template polymorphism to fix soundness issues
    related to universes.

    New unsafe flags to disable locally guard, positivity and universe
    checking. Reliance on these flags is always printed by Print

    Fixed bugs of Export and Import that can have a significant impact
    on user developments (common source of incompatibility!).

    New interactive development method based on vos interface files,
    allowing to work on a file without recompiling the proof parts of
    their dependencies.

    New Arguments annotation for bidirectional type inference
    configuration for reference (e.g. constants, inductive)

    New refine attribute for Instance can be used instead of the
    removed Refine Instance Mode.

    Generalization of the under and over tactics of SSReflect to
    arbitrary relations.

    Revision of the Coq.Reals library, its axiomatisation and
    instances of the constructive and classical real numbers.

Additionally, while the omega tactic is not yet deprecated in this
version of Coq, it should soon be the case and we already recommend
users to switch to lia in new proof scripts (see also the warning
message in the corresponding chapter).

The full (huge) changelog is here:

Revision 1.30 / (download) - annotate - [select for diffs], Fri Jan 24 15:54:48 2020 UTC (3 years, 10 months ago) by jaapb
Branch: MAIN
CVS Tags: pkgsrc-2020Q4-base, pkgsrc-2020Q4, pkgsrc-2020Q3-base, pkgsrc-2020Q3, pkgsrc-2020Q2-base, pkgsrc-2020Q2, pkgsrc-2020Q1-base, pkgsrc-2020Q1
Changes since 1.29: +154 -81 lines
Diff to previous 1.29 (colored)

Updated lang/coq to version 8.10.2.

Changes include:
- native 63-bit machine integers;
- a new sort of definitionally proof-irrelevant propositons: SProp;
- private universes for opaque polymorphic constants;
- string notations and numeral notations;
- a new simplex-based proof engine for the tactics lia, nia, lra and nra;
- new introduction patterns for SSReflect;
- a tactic to rewrite under binders: under;
- easy input of non-ASCII symbols in CoqIDE, which now uses GTK3.

and many small improvements and bugfixes.

Revision 1.29 / (download) - annotate - [select for diffs], Wed Mar 6 09:28:23 2019 UTC (4 years, 9 months ago) by jaapb
Branch: MAIN
CVS Tags: pkgsrc-2019Q4-base, pkgsrc-2019Q4, pkgsrc-2019Q3-base, pkgsrc-2019Q3, pkgsrc-2019Q2-base, pkgsrc-2019Q2, pkgsrc-2019Q1-base, pkgsrc-2019Q1
Changes since 1.28: +2157 -2085 lines
Diff to previous 1.28 (colored)

Updated lang/coq to version 8.9.0.

Many improvements and fixes, but none that appear to break compatibility.
For more details see the CHANGES file.

Revision 1.28 / (download) - annotate - [select for diffs], Thu Aug 2 12:57:03 2018 UTC (5 years, 4 months ago) by jaapb
Branch: MAIN
CVS Tags: pkgsrc-2018Q4-base, pkgsrc-2018Q4, pkgsrc-2018Q3-base, pkgsrc-2018Q3
Changes since 1.27: +393 -158 lines
Diff to previous 1.27 (colored)

Updated package lang/coq to version 8.8.1.

The list of improvements, additions, bugfixes and so on is quite large;
those interested can refer to the CHANGES file in the distribution.

The reference manual has been fully ported to Sphinx.

Revision 1.27 / (download) - annotate - [select for diffs], Sat Jun 16 10:25:51 2018 UTC (5 years, 5 months ago) by markd
Branch: MAIN
CVS Tags: pkgsrc-2018Q2-base, pkgsrc-2018Q2
Changes since 1.26: +2 -2 lines
Diff to previous 1.26 (colored)

coq: always installs coqdoc.sty in tex tree.

Revision 1.26 / (download) - annotate - [select for diffs], Mon Apr 9 11:29:23 2018 UTC (5 years, 7 months ago) by jaapb
Branch: MAIN
Changes since 1.25: +26 -2 lines
Diff to previous 1.25 (colored)

Updated lang/coq to version 8.7.2.

This fixes a critical bug in the VM handling of universes, and adds
various other minor fixes and improvements.

Revision 1.25 / (download) - annotate - [select for diffs], Mon Jan 22 11:54:43 2018 UTC (5 years, 10 months ago) by jaapb
Branch: MAIN
CVS Tags: pkgsrc-2018Q1-base, pkgsrc-2018Q1
Changes since 1.24: +2 -3 lines
Diff to previous 1.24 (colored)

Corrected PLIST for lang/coq

Revision 1.24 / (download) - annotate - [select for diffs], Wed Jan 10 16:26:53 2018 UTC (5 years, 10 months ago) by jaapb
Branch: MAIN
Changes since 1.23: +573 -69 lines
Diff to previous 1.23 (colored)

Updated package lang/coq to version 8.7.1.

This is a compatibility release with OCaml 4.06.0. It also contains many
bugfixes, documentation improvements and user message improvements.

Revision 1.23 / (download) - annotate - [select for diffs], Mon Jan 1 22:29:39 2018 UTC (5 years, 11 months ago) by rillig
Branch: MAIN
Changes since 1.22: +23 -26 lines
Diff to previous 1.22 (colored)

Sort PLIST files.

Unsorted entries in PLIST files have generated a pkglint warning for at
least 12 years. Somewhat more recently, pkglint has learned to sort
PLIST files automatically. Since pkglint 5.4.23, the sorting is only
done in obvious, simple cases. These have been applied by running:

  pkglint -Cnone,PLIST -Wnone,plist-sort -r -F

Revision 1.22 / (download) - annotate - [select for diffs], Fri Nov 3 11:20:28 2017 UTC (6 years, 1 month ago) by jaapb
Branch: MAIN
CVS Tags: pkgsrc-2017Q4-base, pkgsrc-2017Q4
Changes since 1.21: +188 -341 lines
Diff to previous 1.21 (colored)

Updated lang/coq to version 8.7.0.

Includes many improvements and bugfixes (none that seem to be breaking
backwards compatibility though), see the CHANGELOG.
For packaging:
- camlp4 support removed, package now uses camlp5 exclusively
- fix for PR pkg/52651

Revision 1.21 / (download) - annotate - [select for diffs], Fri Sep 8 17:19:01 2017 UTC (6 years, 2 months ago) by jaapb
Branch: MAIN
CVS Tags: pkgsrc-2017Q3-base, pkgsrc-2017Q3
Changes since 1.20: +1998 -1973 lines
Diff to previous 1.20 (colored)

Updated package to latest version, 8.6.1. Changes include:

- Fix #5380: Default colors for CoqIDE are actually applied.
- Fix plugin warnings
- Document named evars (including Show ident)
- Fix Bug #5574, document function scope
- Adding a test case as requested in bug 5205.
- Fix Bug #5568, no dup notation warnings on repeated module imports
- Fix documentation of Typeclasses eauto :=
- Refactor documentation of records.
- Protecting from warnings while compiling 8.6
- Fixing an inconsistency between configure and
- Add test-suite checks for coqchk with constraints
- Fix bug #5019 (looping zify on dependent types)
- Fix bug 5550: "typeclasses eauto with" does not work with section variables.
- Bug 5546, qualify datatype constructors when needed in Show Match
- Bug #5535, test for Show with -emacs
- Fix bug #5486, don't reverse ids in tuples
- Fixing #5522 (anomaly with free vars of pat)
- Fix bug #5526, don't check for nonlinearity in notation if printing only
- Fix bug #5255
- Fix bug #3659: -time should understand multibyte encodings.
- FIx bug #5300: Anomaly: Uncaught exception Not_found" in "Print Assumptions".
- Fix outdated description in RefMan.
- Repairing `Set Rewriting Schemes`
- Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).
- Fix description of command-line arguments for Add (Rec) LoadPath
- Fix bug #5377: @? patterns broken.
- add XML protocol doc
- Fix anomaly when doing [all:Check _.] during a proof.
- Correction of bug #4306
- Fix #5435: [Eval native_compute in] raises anomaly.
- Instances should obey universe binders even when defined by tactics.
- Intern names bound in match patterns
- funind: Ignore missing info for current function
- Do not typecheck twice the type of opaque constants.
- show unused intro pattern warning
- [future] Be eager when "chaining" already resolved future values.
- Opaque side effects
- Fix #5132: coq_makefile generates incorrect install goal
- Run non-tactic comands without resilient_command
- Univs: fix bug #5365, generation of u+k <= v constraints
- make `emit' tail recursive
- Don't require printing-only notation to be productive
- Fix the way setoid_rewrite handles bindings.
- Fix for bug 5244 - set printing width ignored when given enough space
- Fix bug 4969, autoapply was not tagging shelved subgoals correctly

Revision 1.20 / (download) - annotate - [select for diffs], Fri Dec 30 13:23:06 2016 UTC (6 years, 11 months ago) by jaapb
Branch: MAIN
CVS Tags: pkgsrc-2017Q2-base, pkgsrc-2017Q2, pkgsrc-2017Q1-base, pkgsrc-2017Q1
Changes since 1.19: +147 -119 lines
Diff to previous 1.19 (colored)

Updated coq to latest version, 8.6. Changes include:

Changes from V8.6beta1 to V8.6


- Fixed critical bug #5248 in VM long multiplication on 32-bit
  architectures. Was there only since 8.6beta1, so no stable release impacted.

Other bug fixes in universes, type class shelving,...

Changes from V8.5 to V8.6beta1


- A new, faster state-of-the-art universe constraint checker.

Specification language

- Giving implicit arguments explicitly to a constant with multiple
  choices of implicit arguments does not break any more insertion of
  further maximal implicit arguments.
- Ability to put any pattern in binders, prefixed by quote, e.g.
  "fun '(a,b) => ...", "λ '(a,(b,c)), ...", "Definition foo '(x,y) := ...".
  It expands into a "let 'pattern := ..."


- Flag "Bracketing Last Introduction Pattern" is now on by default.
- Flag "Regular Subst Tactic" is now on by default: it respects the
  initial order of hypothesis, it contracts cycles, it unfolds no
  local definitions (common source of incompatibilities, fixable by
  "Unset Regular Subst Tactic").
- New flag "Refolding Reduction", now disabled by default, which turns
  on refolding of constants/fixpoints (as in cbn) during the reductions
  done during type inference and tactic retyping. Can be extremely
  expensive. When set off, this recovers the 8.4 behaviour of unification
  and type inference. Potential source of incompatibility with 8.5 developments
  (the option is set on in Compat/Coq85.v).
- New flag "Shrink Abstract" that minimalizes proofs generated by the abstract
  tactical w.r.t. variables appearing in the body of the proof.
  On by default and deprecated. Minor source of incompatibility
  for code relying on the precise arguments of abstracted proofs.
- Serious bugs are fixed in tactic "double induction" (source of
  incompatibilities as soon as the inductive types have dependencies in
  the type of their constructors; "double induction" remains however
- In introduction patterns of the form (pat1,...,patn), n should match
  the exact number of hypotheses introduced (except for local definitions
  for which pattern can be omitted, as in regular pattern-matching).
- Tactic scopes in Ltac like constr: and ltac: now require parentheses around
  their argument.
- Every generic argument type declares a tactic scope of the form "name:(...)"
  where name is the name of the argument. This generalizes the constr: and ltac:
- When in strict mode (i.e. in a Ltac definition), if the "intro" tactic is
  given a free identifier, it is not bound in subsequent tactics anymore.
  In order to introduce a binding, use e.g. the "fresh" primitive instead
  (potential source of incompatibilities).
- New tactics is_ind, is_const, is_proj, is_constructor for use in Ltac.
- New goal selectors.  Sets of goals can be selected by listing integers
  ranges. Example: "1,4-7,24: tac" focuses "tac" on goals 1,4,5,6,7,24.
- For uniformity with "destruct"/"induction" and for a more natural
  behavior, "injection" can now work in place by activating option
  "Structural Injection". In this case, hypotheses are also put in the
  context in the natural left-to-right order and the hypothesis on
  which injection applies is cleared.
- Tactic "contradiction" (hence "easy") now also solve goals with
  hypotheses of the form "~True" or "t<>t" (possible source of
  incompatibilities because of more successes in automation, but
  generally a more intuitive strategy).
- Option "Injection On Proofs" was renamed "Keep Proof Equalities". When
  enabled, injection and inversion do not drop equalities between objects
  in Prop. Still disabled by default.
- New tactics "notypeclasses refine" and "simple notypeclasses refine" that
  disallow typeclass resolution when typechecking their argument, for use
  in typeclass hints.
- Integration of LtacProf, a profiler for Ltac.
- Reduction tactics now accept more fine-grained flags: iota is now a shorthand
  for the new flags match, fix and cofix.
- The ssreflect subterm selection algorithm is now accessible to tactic writers
  through the ssrmatching plugin.
- When used as an argument of an ltac function, "auto" without "with"
  nor "using" clause now correctly uses only the core hint database by


- Revised the syntax of [Hint Cut] to follow standard notation for regexps.
- Hint Mode now accepts "!" which means that the mode matches only if the
  argument's head is not an evar (it goes under applications, casts, and
  scrutinees of matches and projections).
- Hints can now take an optional user-given pattern, used only by
  [typeclasses eauto] with the [Filtered Unification] option on.


- Many new options and new engine based on the proof monad. The
  [typeclasses eauto] tactic is now a multi-goal, multi-success tactic.
  See reference manual for more information. It is planned to
  replace auto and eauto in the following version. The 8.5 resolution
  engine is still available to help solve compatibility issues.


- The "Shrink Obligations" flag now applies to all obligations, not only
  those solved by the automatic tactic.
- "Shrink Obligations" is on by default and deprecated. Minor source of
  incompatibility for code relying on the precise arguments of


- "Bind Scope" can once again bind "Funclass" and "Sortclass".

General infrastructure

- New configurable warning system which can be controlled with the vernacular
  command "Set Warnings", or, under coqc/coqtop, with the flag "-w". In
  particular, the default is now that warnings are printed by coqc.
- In asynchronous mode, Coq is now capable of recovering from errors and
  continue processing the document.


- coqc accepts a -o option to specify the output file name
- coqtop accepts --print-version to print Coq and OCaml versions in
  easy to parse format
- Setting [Printing Dependent Evars Line] can be unset to disable the
  computation associated with printing the "dependent evars: " line in
  -emacs mode
- Removed the -verbose-compat-notations flag and the corresponding Set
  Verbose Compat vernacular, since these warnings can now be silenced or
  turned into errors using "-w".

XML protocol

- message format has changed, see dev/doc/changes.txt for more details.

Many bug fixes, minor changes and documentation improvements are not mentioned

Changes from V8.5pl2 to V8.5pl3

Critical bugfix

- #4876: Guard checker incompleteness when using primitive projections

Other bugfixes

- #4780: Induction with universe polymorphism on was creating ill-typed terms.
- #4673: regression in setoid_rewrite, unfolding let-ins for type unification.
- #4754: Regression in setoid_rewrite, allow postponed unification problems to remain.
- #4769: Anomaly with universe polymorphic schemes defined inside sections.
- #3886: Program: duplicate obligations of mutual fixpoints.
- #4994: Documentation typo.
- #5008: Use the "md5" command on OpenBSD.
- #5007: Do not assume the "TERM" environment variable is always set.
- #4606: Output a break before a list only if there was an empty line.
- #5001: metas not cleaned properly in clenv_refine_in.
- #2336: incorrect glob data for module symbols (bug #2336).
- #4832: Remove extraneous dot in error message.
- Anomaly in printing a unification error message.
- #4947: Options which take string arguments are not backwards compatible.
- #4156: micromega cache files are now hidden files.
- #4871: interrupting par:abstract kills coqtop.
- #5043: [Admitted] lemmas pick up section variables.
- Fix name of internal refine ("simple refine").
- #5062: probably a typo in Strict Proofs mode.
- #5065: Anomaly: Not a proof by induction.
- Restore native compiler optimizations, they were disabled since 8.5!
- #5077: failure on typing a fixpoint with evars in its type.
- Fix recursive notation bug.
- #5095: non relevant too strict test in let-in abstraction.
- Ensuring that the evar name is preserved by "rename".
- #4887: confusion between using and with in documentation of firstorder.
- Bug in subst with let-ins.
- #4762: eauto weaker than auto.
- Remove if_then_else (was buggy). Use tryif instead.
- #4970: confusion between special "{" and non special "{{" in notations.
- #4529: primitive projections unfolding.
- #4416: Incorrect "Error: Incorrect number of goals".
- #4863: abstract in typeclass hint fails.
- #5123: unshelve can impact typeclass resolution
- Fix a collision about the meta-variable ".." in recursive notations.
- Fix printing of info_auto.
- #3209: Not_found due to an occur-check cycle.
- #5097: status of evars refined by "clear" in ltac: closed wrt evars.
- #5150: Missing dependency of the test-suite subsystems in prerequisite.
- Fix a bug in error printing of unif constraints
- #3941: Do not stop propagation of signals when Coq is busy.
- #4822: Incorrect assertion in cbn.
- #3479 parsing of "{" and "}" when a keyword starts with "{" or "}".
- #5127: Memory corruption with the VM.
- #5102: bullets parsing broken by calls to parse_entry.

Various documentation improvements

Changes from V8.5pl1 to V8.5pl2

Critical bugfix
- Checksums of .vo files dependencies were not correctly checked.
- Unicode-to-ASCII translation was not injective, leading in a soundness bug in
  the native compiler.

Other bugfixes

- #4097: more efficient occur-check in presence of primitive projections
- #4398: type_scope used consistently in "match goal".
- #4450: eauto does not work with polymorphic lemmas
- #4677: fix alpha-conversion in notations needing eta-expansion.
- Fully preserve initial order of hypotheses in "Regular Subst Tactic" mode.
- #4644: a regression in unification.
- #4725: Function (Error: Conversion test raised an anomaly) and Program
  (Error: Cannot infer this placeholder of type)
- #4747: Problem building Coq 8.5pl1 with OCaml 4.03.0: Fatal warnings
- #4752: CoqIDE crash on files not ended by ".v".
- #4777: printing inefficiency with implicit arguments
- #4818: "Admitted" fails due to undefined universe anomaly after calling
- #4823: remote counter: avoid thread race on sockets
- #4841: -verbose flag changed semantics in 8.5, is much harder to use
- #4851: [nsatz] cannot handle duplicated hypotheses
- #4858: Anomaly: Uncaught exception Failure("hd"). Please report. in variant
  of nsatz
- #4880: [nsatz_compute] generates invalid certificates if given redundant
- #4881: synchronizing "Declare Implicit Tactic" with backtrack.
- #4882: anomaly with Declare Implicit Tactic on hole of type with evars
- Fix use of "Declare Implicit Tactic" in refine.
  triggered by CoqIDE
- #4069, #4718: congruence fails when universes are involved.

- Disallow silently dropping universe instances applied to variables
  (forward compatible)
- Allow explicit universe instances on notations, when they can apply
  to the head reference of their expansion.

Build infrastructure
- New update on how to find camlp5 binary and library at configure time.

Revision 1.19 / (download) - annotate - [select for diffs], Sat Jul 2 10:17:18 2016 UTC (7 years, 5 months ago) by jaapb
Branch: MAIN
CVS Tags: pkgsrc-2016Q4-base, pkgsrc-2016Q4, pkgsrc-2016Q3-base, pkgsrc-2016Q3
Changes since 1.18: +2 -2 lines
Diff to previous 1.18 (colored)

Updated package to latest version, 8.5pl1. Also fixed a packaging bug
that had buildlink paths show up in the Coq_config module, and added a
patch from upstream to allow compilation with 4.03.

Critical bugfix
- The subterm relation for the guard condition was incorrectly defined on
  primitive projections (#4588)

Plugin development tools
- add a .merlin target to the makefile

Various performance improvements (time, space used by .vo files)

Other bugfixes

- Fix order of arguments to Big.compare_case in ExtrOcamlZBigInt.v
- Added compatibility coercions from Specif.v which were present in Coq 8.4.
- Fixing a source of inefficiency and an artificial dependency in the printer in the congruence tactic.
- Allow to unset the refinement mode of Instance in ML
- Fixing an incorrect use of prod_appvect on a term which was not a product in setoid_rewrite.
- Add -compat 8.4 econstructor tactics, and tests
- Add compatibility Nonrecursive Elimination Schemes
- Fixing the "No applicable tactic" non informative error message regression on apply.
- Univs: fix get_current_context (bug #4603, part I)
- Fix a bug in Program coercion code
- Fix handling of arity of definitional classes.
- #4630: Some tactics are 20x slower in 8.5 than 8.4.
- #4627: records with no declared arity can be template polymorphic.
- #4623: set tactic too weak with universes (regression)
- Fix incorrect behavior of CS resolution
- #4591: Uncaught exception in directory browsing.
- CoqIDE is more resilient to initialization errors.
- #4614: "Fully check the document" is uninterruptable.
- Try eta-expansion of records only on non-recursive ones
- Fix bug when a sort is ascribed to a Record
- Primitive projections: protect kernel from erroneous definitions.
- Fixed bug #4533 with previous Keyed Unification commit
- Win: kill unreliable hence do not waitpid after kill -9 (Close #4369)
- Fix strategy of Keyed Unification
- #4608: Anomaly "output_value: abstract value (outside heap)".
- #4607: do not read native code files if native compiler was disabled.
- #4105: poor escaping in the protocol between CoqIDE and coqtop.
- #4596: [rewrite] broke in the past few weeks.
- #4533 (partial): respect declared global transparency of projections in
- #4544: Backtrack on using full betaiota reduction during keyed unification.
- #4540: CoqIDE bottom progress bar does not update.
- Fix regression from 8.4 in reflexivity
- #4580: [Set Refine Instance Mode] also used for Program Instance.
- #4582: cannot override notation [ x ]. MAY CREATE INCOMPATIBILITIES, see #4683.
- STM: Print/Extraction have to be skipped if -quick
- #4542: CoqIDE: STOP button also stops workers
- STM: classify some variants of Instance as regular `Fork nodes.
- #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity").
- Do not give a name to anonymous evars anymore. See bug #4547.
- STM: always stock in vio files the first node (state) of a proof
- STM: not delegate proofs that contain Vernac(Module|Require|Import), #4530
- Don't fail fatally if PATH is not set.
- #4537: Coq 8.5 is slower in typeclass resolution.
- #4522: Incorrect "Warning..." on windows.
- #4373: coqdep does not know about .vio files.
- #3826: "Incompatible module types" is uninformative.
- #4495: Failed assertion in
- #4511: evar tactic can create non-typed evars.
- #4503: mixing universe polymorphic and monomorphic variables and definitions in sections is unsupported.
- #4519: oops, global shadowed local universe level bindings.
- #4506: Anomaly: File "pretyping/", line 169, characters 14-20: Assertion failed.
- #4548: Coqide crashes when going back one command

Revision 1.18 / (download) - annotate - [select for diffs], Sat Feb 6 16:08:36 2016 UTC (7 years, 9 months ago) by jaapb
Branch: MAIN
CVS Tags: pkgsrc-2016Q2-base, pkgsrc-2016Q2, pkgsrc-2016Q1-base, pkgsrc-2016Q1
Changes since 1.17: +3166 -179 lines
Diff to previous 1.17 (colored)

Updated package to latest version, 8.5. The changeset is over 500 lines
long, so I will not include it here, but details can be found in the
CHANGES file in the source. (the previous version was V8.4.)

Revision 1.17 / (download) - annotate - [select for diffs], Tue Dec 29 06:22:21 2015 UTC (7 years, 11 months ago) by dholland
Branch: MAIN
Changes since 1.16: +4 -4 lines
Diff to previous 1.16 (colored)


Revision 1.16 / (download) - annotate - [select for diffs], Sat Apr 25 13:41:18 2015 UTC (8 years, 7 months ago) by jaapb
Branch: MAIN
CVS Tags: pkgsrc-2015Q4-base, pkgsrc-2015Q4, pkgsrc-2015Q3-base, pkgsrc-2015Q3, pkgsrc-2015Q2-base, pkgsrc-2015Q2
Changes since 1.15: +2 -1 lines
Diff to previous 1.15 (colored)

Updated coq to version 8.4pl6. Changes from previous version include (apart
from bugfixes):

- Coq compilation made possible with forthcoming ocaml 4.03.
- command for locating exists notation in refman changed.
- Various improvements of the Reference Manual (especially its html version)
- implicit arguments of local definitions fixed (possible
  source of incompatibilities).
- New command "Print Debug GC".
- Function cannot define graph.
- Optimizing compilation of pattern matching.
- Better inference of impossible cases in pattern-matching.
- Evar leak in pattern-matching compilation
- ill-typed replacement in "change ... with ...".
- unbound evars in "change ... with ...".
- wrong return clause of a match pattern in Ltac.
- cleared local hints for autounfold.
- cleared local hints for autounfold.
- lost evars in "change ... with ...".
- supporting let-ins in constructors for vm_compute
- unfortunate typo in compare_height.
- unfortunate typos in absorption lemmas over bool.
- Full support of utf8 Greek letters (block U0370) in coqdoc

Revision 1.15 / (download) - annotate - [select for diffs], Thu Oct 9 22:19:01 2014 UTC (9 years, 1 month ago) by jaapb
Branch: MAIN
CVS Tags: pkgsrc-2015Q1-base, pkgsrc-2015Q1, pkgsrc-2014Q4-base, pkgsrc-2014Q4
Changes since 1.14: +5 -5 lines
Diff to previous 1.14 (colored)

Revbump because of ocaml 4.02, added compilation patch (already in
repository upstream) and updated package to use framework.

Revision 1.14 / (download) - annotate - [select for diffs], Wed Oct 30 00:21:49 2013 UTC (10 years, 1 month ago) by minskim
Branch: MAIN
CVS Tags: pkgsrc-2014Q3-base, pkgsrc-2014Q3, pkgsrc-2014Q2-base, pkgsrc-2014Q2, pkgsrc-2014Q1-base, pkgsrc-2014Q1, pkgsrc-2013Q4-base, pkgsrc-2013Q4
Changes since 1.13: +2 -2 lines
Diff to previous 1.13 (colored)

Install a LaTeX style file into texmf-dist, not texmf.

The latter has been deprecated in TeX Live 2013.

Revision 1.13 / (download) - annotate - [select for diffs], Fri Nov 16 14:44:22 2012 UTC (11 years ago) by jaapb
Branch: MAIN
CVS Tags: pkgsrc-2013Q3-base, pkgsrc-2013Q3, pkgsrc-2013Q2-base, pkgsrc-2013Q2, pkgsrc-2013Q1-base, pkgsrc-2013Q1, pkgsrc-2012Q4-base, pkgsrc-2012Q4
Changes since 1.12: +892 -4 lines
Diff to previous 1.12 (colored)

Updated package to add 'doc' option and (if given) build documentation, as
requested in PR pkg/47152. Bumped PKGREVISION.

Revision 1.12 / (download) - annotate - [select for diffs], Mon Oct 29 11:33:17 2012 UTC (11 years, 1 month ago) by jaapb
Branch: MAIN
Changes since 1.11: +131 -43 lines
Diff to previous 1.11 (colored)

Taken over maintainership (as discussed with previous maintainer, Updated package to use PLIST_VARS and CONF_FILES.
Updated coq to version 8.4. Changes include:

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

Revision 1.11 / (download) - annotate - [select for diffs], Sun Nov 14 20:53:02 2010 UTC (13 years ago) by tonio
Branch: MAIN
CVS Tags: pkgsrc-2012Q3-base, pkgsrc-2012Q3, pkgsrc-2012Q2-base, pkgsrc-2012Q2, pkgsrc-2012Q1-base, pkgsrc-2012Q1, pkgsrc-2011Q4-base, pkgsrc-2011Q4, pkgsrc-2011Q3-base, pkgsrc-2011Q3, pkgsrc-2011Q2-base, pkgsrc-2011Q2, pkgsrc-2011Q1-base, pkgsrc-2011Q1, pkgsrc-2010Q4-base, pkgsrc-2010Q4
Changes since 1.10: +359 -172 lines
Diff to previous 1.10 (colored)

Update lang/coq to 8.3

Main changes:
Includes a new tactic (nsatz, standing for Hilbert's NullStellensatz, that
extends ring to systems of polynomial equations) and a few new libraries (a
certification of mergesort, a new library of finite sets with computational and
logical contents separated).

This version also comes with many improvements of existing features, especially
regarding the tactics, the module system, extraction, the type classes, the
program command, libraries, coqdoc. Here is an excerpt:
* new operator <+ for conveniently chaining application of functors
* new round of extension of the modular library of arithmetic
* support for matching terms with binders in Ltac,
* linking notations in coqdoc,
* quote tactic now working on arbitrary expressions,
* Lemma and co accept parameters that are automatically introduced,
* interactive proofs in module types,
* a beautifying coqc option for pretty-printing files

See the file CHANGES for a full log of changes.

Revision 1.10 / (download) - annotate - [select for diffs], Sat Sep 5 20:44:57 2009 UTC (14 years, 3 months ago) by tonio
Branch: MAIN
CVS Tags: pkgsrc-2010Q3-base, pkgsrc-2010Q3, pkgsrc-2010Q2-base, pkgsrc-2010Q2, pkgsrc-2010Q1-base, pkgsrc-2010Q1, pkgsrc-2009Q4-base, pkgsrc-2009Q4, pkgsrc-2009Q3-base, pkgsrc-2009Q3
Changes since 1.9: +446 -59 lines
Diff to previous 1.9 (colored)

Update lang/coq to 8.2pl1

Changes from V8.1 to V8.2


- If a fixpoint is not written with an explicit { struct ... }, then
  all arguments are tried successively (from left to right) until one is
  found that satisfies the structural decreasing condition.
- New experimental typeclass system giving ad-hoc polymorphism and
  overloading based on dependent records and implicit arguments.
- New syntax "let 'pat := b in c" for let-binding using irrefutable patterns.
- New syntax "forall {A}, T" for specifying maximally inserted implicit
  arguments in terms.
- Sort of Record/Structure, Inductive and CoInductive defaults to Type
  if omitted.
- Support for optional "where" notation clauses for record fields.
- (Co)Inductive types can be defined as records
  (e.g. "CoInductive stream := { hd : nat; tl : stream }.")
- New syntax "Theorem id1:t1 ... with idn:tn" for proving mutually dependent
- Support for sort-polymorphism on constants denoting inductive types.
- Several evolutions of the module system (handling of module aliases,
  functorial module types, an Include feature, etc).
- Prop now a subtype of Set (predicative and impredicative forms).
- Recursive inductive types in Prop with a single constructor of which
  all arguments are in Prop is now considered to be a singleton
  type. It consequently supports all eliminations to Prop, Set and Type.
  As a consequence, Acc_rect has now a more direct proof [possible source
  of easily fixed incompatibility in case of manual definition of a recursor
  in a recursive singleton inductive type].
- New syntax to do implicit generalization in binders and inside terms.
- New tentative syntax for introduction of record objects without mentioning
  the constructor {| field := body; ... |}, turning missing fields into holes
  (compatible with refine and Program).

Vernacular commands

- Added option Global to "Arguments Scope" for section surviving.
- Added option "Unset Elimination Schemes" to deactivate the automatic
  generation of elimination schemes.
- Modification of the Scheme command so you can ask for the name to be
  automatically computed (e.g. Scheme Induction for nat Sort Set).
- New command "Combined Scheme" to build combined mutual induction
  principles from existing mutual induction principles.
- New command "Scheme Equality" to build a decidable (boolean) equality
  for simple inductive datatypes and a decision property over this equality
  (e.g.  Scheme Equality for nat).
- Added option "Set Equality Scheme" to make automatic the declaration
  of the boolean equality when possible.
- Source of universe inconsistencies now printed when option
  "Set Printing Universes" is activated.
- New option "Set Printing Existential Instances" for making the display of
  existential variable instances explicit.
- Support for option "[id1 ... idn]", and "-[id1 ... idn]", for the
  "compute"/"cbv" reduction strategy, respectively meaning reduce only, or
  everything but, the constants id1 ... idn. "lazy" alone or followed by
  "[id1 ... idn]", and "-[id1 ... idn]" also supported, meaning apply
  all of beta-iota-zeta-delta, possibly restricting delta.
- New command "Strategy" to control the expansion of constants during
  conversion tests. It generalizes commands Opaque and Transparent by
  introducing a range of levels. Lower levels are assigned to constants
  that should be expanded first.
- New options Global and Local to Opaque and Transparent.
- New command "Print Assumptions" to display all variables, parameters
  or axioms a theorem or definition relies on.
- "Add Rec LoadPath" now provides references to libraries using partially
  qualified names (this holds also for coqtop/coqc option -R).
- SearchAbout supports negated search criteria, reference to logical objects
  by their notation, and more generally search of subterms.
- "Declare ML Module" now allows to import .cmxs files when Coq is
  compiled in native code with a version of OCaml that supports native
  Dynlink (>= 3.11).
- New command "Create HintDb name [discriminated]" to explicitely declare
  a new hint database and optionaly turn on a discrimination net
  implementation to index all the lemmas in the database.
- New commands "Hint Transparent" and "Hint Opaque" to set the unfolding
  status of definitions used by auto. This information is taken into account
  by the discrimination net and the unification algorithm.
- "Hint Extern" now takes an optional pattern and applies the given tactic
  all the time if no pattern is given.
- Specific sort constraints on Record now taken into account.
- "Print LoadPath" supports a path argument to filter the display.


- Several parts of the libraries are now in Type, in particular FSets,
  SetoidList, ListSet, Sorting, Zmisc. This may induce a few
  incompatibilities. In case of trouble while fixing existing development,
  it may help to simply declare Set as an alias for Type (see file
- New arithmetical library in theories/Numbers. It contains:
  * an abstract modular development of natural and integer arithmetics
    in Numbers/Natural/Abstract and Numbers/Integer/Abstract
  * an implementation of efficient computational bounded and unbounded
    integers that can be mapped to processor native arithmetics.
    See Numbers/Cyclic/Int31 for 31-bit integers and Numbers/Natural/BigN
    for unbounded natural numbers and Numbers/Integer/BigZ for unbounded
  * some proofs that both older libraries Arith, ZArith and NArith and
    newer BigN and BigZ implement the abstract modular development.
    This allows in particular BigN and BigZ to already come with a
    large database of basic lemmas and some generic tactics (ring),
  This library has still an experimental status, as well as the
  processor-acceleration mechanism, but both its abstract and its
  concrete parts are already quite usable and could challenge the use
  of nat, N and Z in actual developments. Moreover, an extension of
  this framework to rational numbers is ongoing, and an efficient
  Q structure is already provided (see Numbers/Rational/BigQ), but
  this part is currently incomplete (no abstract layer and generic
- Many changes in FSets/FMaps. In practice, compatibility with earlier
  version should be fairly good, but some adaptations may be required.
  * Interfaces of unordered ("weak") and ordered sets have been factorized
    thanks to new features of Coq modules (in particular Include), see
    FSetInterface. Same for maps. Hints in these interfaces have been
    reworked (they are now placed in a "set" database).
  * To allow full subtyping between weak and ordered sets, a field
    "eq_dec" has been added to OrderedType. The old version of OrderedType
    is now called MiniOrderedType and functor MOT_to_OT allow to
    convert to the new version. The interfaces and implementations
    of sets now contain also such a "eq_dec" field.
  * FSetDecide, contributed by Aaron Bohannon, contains a decision
    procedure allowing to solve basic set-related goals (for instance,
    is a point in a particular set ?). See FSetProperties for examples.
  * Functors of properties have been improved, especially the ones about
    maps, that now propose some induction principles. Some properties
    of fold need less hypothesis.
  * More uniformity in implementations of sets and maps: they all use
    implicit arguments, and no longer export unnecessary scopes (see
    bug #1347)
  * Internal parts of the implementations based on AVL have evolved a
    lot. The main files FSetAVL and FMapAVL are now much more
    lightweight now. In particular, minor changes in some functions
    has allowed to fully separate the proofs of operational
    correctness from the proofs of well-balancing: well-balancing is
    critical for efficiency, but not anymore for proving that these
    trees implement our interfaces, hence we have moved these proofs
    into appendix files FSetFullAVL and FMapFullAVL. Moreover, a few
    functions like union and compare have been modified in order to be
    structural yet efficient. The appendix files also contains
    alternative versions of these few functions, much closer to the
    initial Ocaml code and written via the Function framework.
- Library IntMap, subsumed by FSets/FMaps, has been removed from
  Coq Standard Library and moved into a user contribution Cachan/IntMap
- Better computational behavior of some constants (eq_nat_dec and
  le_lt_dec more efficient, Z_lt_le_dec and
  transparent, ...) (exceptional source of incompatibilities).
- Boolean operators moved from module Bool to module Datatypes (may need
  to rename qualified references in script and force notations || and &&
  to be at levels 50 and 40 respectively).
- The constructors xI and xO of type positive now have postfix notations
  "~1" and "~0", allowing to write numbers in binary form easily, for instance
  6 is 1~1~0 and 4*p is p~0~0 (see BinPos.v).
- Improvements to NArith (Nminus, Nmin, Nmax), and to QArith (in particular
  a better power function).
- Changes in ZArith: several additional lemmas (used in theories/Numbers),
  especially in Zdiv, Znumtheory, Zpower. Moreover, many results in
  Zdiv have been generalized: the divisor may simply be non-null
  instead of strictly positive (see lemmas with name ending by
  "_full"). An alternative file ZOdiv proposes a different behavior
  (the one of Ocaml) when dividing by negative numbers.
- Changes in Arith: EqNat and Wf_nat now exported from Arith, some
  constructions on nat that were outside Arith are now in (e.g. iter_nat).
- In SetoidList, eqlistA now expresses that two lists have similar elements
  at the same position, while the predicate previously called eqlistA
  is now equivlistA (this one only states that the lists contain the same
  elements, nothing more).
- Changes in Reals:
  * Most statement in "sigT" (including the
    completeness axiom) are now in "sig" (in case of incompatibility,
    use proj1_sig instead of projT1, sig instead of sigT, etc).
  * More uniform naming scheme (identifiers in French moved to English,
    consistent use of 0 -- zero -- instead of O -- letter O --, etc).
  * Lemma on prod_f_SO is now on prod_f_R0.
  * Useless hypothesis of ln_exists1 dropped.
  * New Rlogic.v states a few logical properties about R axioms.
  * RIneq.v extended and made cleaner.
- Slight restructuration of the Logic library regarding choice and classical
  logic. Addition of files providing intuitionistic axiomatizations of
  descriptions: Epsilon.v, Description.v and IndefiniteDescription.v.
- Definition of pred and minus made compatible with the structural
  decreasing criterion for use in fixpoints.
- Files Relations/Rstar.v and Relations/Newman.v moved out to the user
  contribution repository (contribution CoC_History). New lemmas about
  transitive closure added and some bound variables renamed (exceptional
  risk of incompatibilities).

Notations, coercions, implicit arguments and type inference

- More automation in the inference of the return clause of dependent
  pattern-matching problems.
- Experimental allowance for omission of the clauses easily detectable as
  impossible in pattern-matching problems.
- Improved inference of implicit arguments, now working inside record
- New options "Set Maximal Implicit Insertion", "Set Reversible Pattern
  Implicit", "Set Strongly Strict Implicit" and "Set Printing Implicit
  Defensive" for controlling inference and use of implicit arguments.
- New modifier in "Implicit Arguments" to force an implicit argument to
  be maximally inserted.
- New options Global and Local to "Implicit Arguments" for section
  surviving or non export outside module.
- Level "constr" moved from 9 to 8.
- Structure/Record now printed as Record (unless option Printing All is set).
- Support for parametric notations defining constants.
- Insertion of coercions below product types refrains to unfold
  constants (possible source of incompatibility).
- New support for fix/cofix in notations.

Tactic Language

- Second-order pattern-matching now working in Ltac "match" clauses
  (syntax for second-order unification variable is "@?X").
- Support for matching on let bindings in match context using syntax
  "H := body" or "H := body : type".
- (?X ?Y) patterns now match any application instead of only unary
  applications (possible source of incompatibility).
- Ltac accepts integer arguments (syntax is "ltac:nnn" for nnn an integer).
- The general sequence tactical "expr_0 ; [ expr_1 | ... | expr_n ]"
  is extended so that at most one expr_i may have the form "expr .."
  or just "..". Also, n can be different from the number of subgoals
  generated by expr_0. In this case, the value of expr (or idtac in
  case of just "..") is applied to the intermediate subgoals to make
  the number of tactics equal to the number of subgoals.
- A name used as the name of the parameter of a lemma (like f in
  "apply f_equal with (f:=t)") is now interpreted as a ltac variable
  if such a variable exists (this is a possible source of
  incompatibility and it can be fixed by renaming the variables of a
  ltac function into names that do not clash with the lemmas
  parameter names used in the tactic).
- New syntax "Ltac tac ::= ..." to rebind a tactic to a new expression.
- "let rec ... in ... " now supported for expressions without explicit
  parameters; interpretation is lazy to the contrary of "let ... in ...";
  hence, the "rec" keyword can be used to turn the argument of a
  "let ... in ..." into a lazy one.
- Patterns for hypotheses types in "match goal" are now interpreted in
- A bound variable whose name is not used elsewhere now serves as
  metavariable in "match" and it gets instantiated by an identifier
  (allow e.g. to extract the name of a statement like "exists x, P x").
- New printing of Ltac call trace for better debugging.
- The C-zar (formerly know as declarative) proof language is now properly


- New tactics "apply -> term", "apply <- term", "apply -> term in
  ident", "apply <- term in ident" for applying equivalences (iff).
- "apply" and "rewrite" now take open terms (terms with undefined existentials)
  as input.
- Slight improvement of the hnf and simpl tactics when applied on
  expressions with explicit occurrences of match or fix.
- New tactics "eapply in", "erewrite", "erewrite in".
- New tactics "ediscriminate", "einjection", "esimplify_eq".
- Tactics "discriminate", "injection", "simplify_eq" now support any
  term as argument. Clause "with" is also supported.
- Unfoldable references can be given by notation's string rather than by name
  in unfold.
- The "with" arguments are now typed using informations from the current goal:
  allows support for coercions and more inference of implicit arguments.
- Application of "f_equal"-style lemmas works better.
- Tactics elim, case, destruct and induction now support variants eelim,
  ecase, edestruct and einduction.
- Tactics destruct and induction now support the "with" option and the
  "in" clause option. If the option "in" is used, an equality is added
  to remember the term to which the induction or case analysis applied
  (possible source of parsing incompatibilities when destruct or induction is
   part of a let-in expression in Ltac; extra parentheses are then required).
- New support for "as" clause in tactics "apply in" and "eapply in".
- Some new intro patterns:
  * intro pattern "?A" genererates a fresh name based on A.
    Caveat about a slight loss of compatibility:
    Some intro patterns don't need space between them. In particular
    intros ?a?b used to be legal and equivalent to intros ? a ? b. Now it
    is still legal but equivalent to intros ?a ?b.
  * intro pattern "(A & ... & Y & Z)" synonym to "(A,....,(Y,Z)))))"
    for right-associative constructs like /\ or exists.
- Several syntax extensions concerning "rewrite":
  * "rewrite A,B,C" can be used to rewrite A, then B, then C. These rewrites
    occur only on the first subgoal: in particular, side-conditions of the
    "rewrite A" are not concerned by the "rewrite B,C".
  * "rewrite A by tac" allows to apply tac on all side-conditions generated by
    the "rewrite A".
  * "rewrite A at n" allows to select occurrences to rewrite: rewrite only
    happen at the n-th exact occurrence of the first successful matching of
    A in the goal.
  * "rewrite 3 A" or "rewrite 3!A" is equivalent to "rewrite A,A,A".
  * "rewrite !A" means rewriting A as long as possible (and at least once).
  * "rewrite 3?A" means rewriting A at most three times.
  * "rewrite ?A" means rewriting A as long as possible (possibly never).
  * many of the above extensions can be combined with each other.
- Introduction patterns better respect the structure of context in presence of
  missing or extra names in nested disjunction-conjunction patterns [possible
  source of rare incompatibilities].
- New syntax "rename a into b, c into d" for "rename a into b; rename c into d"
- New tactics "dependent induction/destruction H [ generalizing id_1 .. id_n ]"
  to do induction-inversion on instantiated inductive families ? la BasicElim.
- Tactics "apply" and "apply in" now able to reason modulo unfolding of
  constants (possible source of incompatibility in situations where apply
  may fail, e.g. as argument of a try or a repeat and in a ltac function);
  versions that do not unfold are renamed into "simple apply" and
  "simple apply in" (usable for compatibility or for automation).
- Tactics "apply" and "apply in" now able to traverse conjunctions and to
  select the first matching lemma among the components of the conjunction;
  tactic "apply" also able to apply lemmas of conclusion an empty type.
- Tactic "apply" now supports application of several lemmas in a row.
- Tactics "set" and "pose" can set functions using notation "(f x1..xn := c)".
- New tactic "instantiate" (without argument).
- Tactic firstorder "with" and "using" options have their meaning swapped for
  consistency with auto/eauto (source of incompatibility).
- Tactic "generalize" now supports "at" options to specify occurrences
  and "as" options to name the quantified hypotheses.
- New tactic "specialize H with a" or "specialize (H a)" allows to transform
  in-place a universally-quantified hypothesis (H : forall x, T x) into its
  instantiated form (H : T a). Nota: "specialize" was in fact there in earlier
  versions of Coq, but was undocumented, and had a slightly different behavior.
- New tactic "contradict H" can be used to solve any kind of goal as long as
  the user can provide afterwards a proof of the negation of the hypothesis H.
  If H is already a negation, say ~T, then a proof of T is asked.
  If the current goal is a negation, say ~U, then U is saved in H afterwards,
  hence this new tactic "contradict" extends earlier tactic "swap", which is
  now obsolete.
- Tactics f_equal is now done in ML instead of Ltac: it now works on any
  equality of functions, regardless of the arity of the function.
- New options "before id", "at top", "at bottom" for tactics "move"/"intro".
- Some more debug of reflexive omega (romega), and internal clarifications.
  Moreover, romega now has a variant "romega with *" that can be also used
  on non-Z goals (nat, N, positive) via a call to a translation tactic named
  zify (its purpose is to Z-ify your goal...). This zify may also be used
  independantly of romega.
- Tactic "remember" now supports an "in" clause to remember only selected
  occurrences of a term.
- Tactic "pose proof" supports name overwriting in case of specialization of an
- Semi-decision tactic "jp" for first-order intuitionistic logic moved to user
  contributions (subsumed by "firstorder").


- Moved useful tactics in theories/Program and documented them.
- Add Program.Basics which contains standard definitions for functional
  programming (id, apply, flip...)
- More robust obligation handling, dependent pattern-matching and
  well-founded definitions.
- Program CoFixpoint is accepted, Program Fixpoint uses the new way to infer
  which argument decreases structurally.
- Program Lemma, Axiom etc... now permit to have obligations in the statement
  iff they can be automatically solved by the default tactic.
- Renamed "Obligations Tactic" command to "Obligation Tactic".
- New command "Preterm [ of id ]" to see the actual term fed to Coq for
  debugging purposes.
- New option "Transparent Obligations" to control the declaration of
  obligations as transparent or opaque. All obligations are now transparent
  by default, otherwise the system declares them opaque if possible.
- Changed the notations "left" and "right" to "in_left" and "in_right" to hide
  the proofs in standard disjunctions, to avoid breaking existing scripts when
  importing Program. Also, put them in program_scope.

Type Classes

- New "Class", "Instance" and "Program Instance" commands to define
  classes and instances documented in the reference manual.
- New binding construct "`{Class_1 param_1 .. param_n, Class_2 ...}"
  for binding type classes, usable everywhere.
- New command " Print Classes " and " Print Instances some_class " to
  print tables for typeclasses.
- New default eauto hint database "typeclass_instances" used by the default
  typeclass instance search tactic.
- New theories directory "theories/Classes" for standard typeclasses
  declarations. Module Classes.RelationClasses is a typeclass port of
  Relation_Definitions plus a generic development of algebra on
  n-ary heterogeneous predicates.

Setoid rewriting

- Complete (and still experimental) rewrite of the tactic
  based on typeclasses. The old interface and semantics are
  almost entirely respected, except:

  - Import Setoid is now mandatory to be able to call setoid_replace
  and declare morphisms.

  - "-->", "++>" and "==>" are now right associative notations
  declared at level 55 in scope signature_scope.
  Their introduction may break existing scripts that defined
  them as notations with different levels.

  - One can use [Typeclasses Opaque/Transparent [cst]] to indicate
  that [cst] should not be unfolded during unification for morphism
  resolution, by default all constants are transparent.

  - The [setoid_rewrite]'s semantics change when rewriting with
  a lemma: it can rewrite two different instantiations of the lemma
  at once. Use [setoid_rewrite H at 1] for (almost) the usual semantics.
  [setoid_rewrite] will also try to rewrite under binders now, and can
  succeed on different terms than before. In particular, it will unify under
  let-bound variables. When called through [rewrite], the semantics are
  unchanged though.

  - [Add Morphism term : id] has different semantics when used with
  parametric morphism: it will try to find a relation on the parameters
  too. The behavior has also changed with respect to default relations:
  the most recently declared Setoid/Relation will be used, the documentation
  explains how to customize this behavior.

  - Parametric Relation and Morphism are declared differently, using the
  new [Add Parametric] commands, documented in the manual.

  - Setoid_Theory is now an alias to Equivalence, scripts building objects
  of type Setoid_Theory need to unfold (or [red]) the definitions
  of Reflexive, Symmetric and Transitive in order to get the same goals
  as before. Scripts which introduced variables explicitely will not break.

  - The order of subgoals when doing [setoid_rewrite] with side-conditions
  is now always the same: first the new goal, then the conditions.

- New standard library modules Classes.Morphisms declares
  standard morphisms on refl/sym/trans relations.
  Classes.Morphisms_Prop declares morphisms on propositional
  connectives and Classes.Morphisms_Relations on generalized predicate
  connectives. Classes.Equivalence declares notations and tactics
  related to equivalences and Classes.SetoidTactics defines the
  setoid_replace tactics and some support for the "Add *" interface,
  notably the tactic applied automatically before each "Add Morphism"

- User-defined subrelations are supported, as well as higher-order morphisms
  and rewriting under binders. The tactic is also extensible entirely in Ltac.
  The documentation has been updated to cover these features.

- [setoid_rewrite] and [rewrite] now support the [at] modifier to select
  occurrences to rewrite, and both use the [setoid_rewrite] code, even when
  rewriting with leibniz equality if occurrences are specified.


- Improved behavior of the Caml extraction of modules: name clashes should
  not happen anymore.
- The command Extract Inductive has now a syntax for infix notations. This
  allows in particular to map Coq lists and pairs onto Caml ones:
    Extract Inductive list => list [ "[]" "(::)" ].
    Extract Inductive prod => "(*)" [ "(,)" ].
- In pattern matchings, a default pattern "| _ -> ..." is now used whenever
  possible if several branches are identical. For instance, functions
  corresponding to decidability of equalities are now linear instead of
- A new instruction Extraction Blacklist id1 .. idn allows to prevent filename
  conflits with existing code, for instance when extracting module List
  to Ocaml.


- CoqIDE font defaults to monospace so as indentation to be meaningful.
- CoqIDE supports nested goals and any other kind of declaration in the middle
  of a proof.
- Undoing non-tactic commands in CoqIDE works faster.
- New CoqIDE menu for activating display of various implicit informations.
- Added the possibility to choose the location of tabs in coqide:
  (in Edit->Preferences->Misc)
- New Open and Save As dialogs in CoqIDE which filter *.v files.


- New stand-alone .vo files verifier "coqchk".
- Extended -I coqtop/coqc option to specify a logical dir: "-I dir -as coqdir".
- New coqtop/coqc option -exclude-dir to exclude subdirs for option -R.
- The binary "parser" has been renamed to "coq-parser".

- Improved coqdoc and dump of globalization information to give more
  meta-information on identifiers. All categories of Coq definitions are
  supported, which makes typesetting trivial in the generated documentation.
- A "--interpolate" option permits to use typesetting information from the
  typechecked part of the file to typeset identifiers appearing in Coq escapings
  inside the documentation.
- Better handling of utf8 ("--utf8" option) and respect of spaces in the source.
- Support for hyperlinking and indexing developments in the TeX output.
- New option "color" of the coqdoc style file to render identifiers using colors.
- Additional macros in the TeX ouput allowing to customize indentation and size of
  empty lines. New environment "coqdoccode" for Coq code.


- Coq installation provides enough files so that Ocaml's extensions need not
  the Coq sources to be compiled (this assumes O'Caml 3.10 and Camlp5).
- New commands "Set Whelp Server" and "Set Whelp Getter" to customize the
  Whelp search tool.
- Syntax of "Test Printing Let ref" and "Test Printing If ref" changed into
  "Test Printing Let for ref" and "Test Printing If for ref".
- An overhauled build system (new Makefiles); see dev/doc/build-system.txt.
- Add -browser option to configure script.
- Build a shared library for the C part of Coq, and use it by default on
  non-(Windows or MacOS) systems. Bytecode executables are now pure. The
  behaviour is configurable with -coqrunbyteflags, -coqtoolsbyteflags and
  -custom configure options.
- Complexity tests can be skipped by setting the environment variable

Revision 1.9 / (download) - annotate - [select for diffs], Sun Jun 14 20:34:13 2009 UTC (14 years, 5 months ago) by joerg
Branch: MAIN
CVS Tags: pkgsrc-2009Q2-base, pkgsrc-2009Q2
Changes since 1.8: +2 -2 lines
Diff to previous 1.8 (colored)

Replace @exec/@unexec with @pkgdir or drop it.

Revision 1.8 / (download) - annotate - [select for diffs], Sun Jun 14 18:03:29 2009 UTC (14 years, 5 months ago) by joerg
Branch: MAIN
Changes since 1.7: +1 -36 lines
Diff to previous 1.7 (colored)

Remove @dirrm entries from PLISTs

Revision 1.7 / (download) - annotate - [select for diffs], Sat Apr 12 22:43:02 2008 UTC (15 years, 7 months ago) by jlam
Branch: MAIN
CVS Tags: pkgsrc-2009Q1-base, pkgsrc-2009Q1, pkgsrc-2008Q4-base, pkgsrc-2008Q4, pkgsrc-2008Q3-base, pkgsrc-2008Q3, pkgsrc-2008Q2-base, pkgsrc-2008Q2, cwrapper, cube-native-xorg-base, cube-native-xorg
Changes since 1.6: +3 -3 lines
Diff to previous 1.6 (colored)

Convert to use PLIST_VARS instead of manually passing "@comment "
through PLIST_SUBST to the plist module.

Revision 1.6 / (download) - annotate - [select for diffs], Sat Dec 1 13:05:36 2007 UTC (16 years ago) by tonio
Branch: MAIN
CVS Tags: pkgsrc-2008Q1-base, pkgsrc-2008Q1, pkgsrc-2007Q4-base, pkgsrc-2007Q4
Changes since 1.5: +3 -1 lines
Diff to previous 1.5 (colored)

Update lang/coq to 8.2pl2

As camlp5 is required with ocaml 3.10, bring it as a dependency anyway,
instead of requiring ocaml 3.10

Changes include:
* Installation
- Support for compilation with ocaml 3.10 and (transitional) camlp5.
- Many bugs have been fixed (cf coq-bugs web page)
- All known failures of ROmega have been fixed. It should now be a
  faithful and quicker replacement for Omega (except when nat parts
  are involved). ROmega and Omega now handle <->.
- Better computational behavior of some constants (eq_nat_dec and
  le_lt_dec more efficient, Z_lt_le_dec and
  transparent) [exceptionally source of incompatibilities].
- Loading FSets/FMap used to open unwanted scopes of integer datatypes
  (see bug #1347). These scopes may need to be manually opened now.

Revision 1.5 / (download) - annotate - [select for diffs], Sun Feb 25 15:03:52 2007 UTC (16 years, 9 months ago) by tonio
Branch: MAIN
CVS Tags: pkgsrc-2007Q3-base, pkgsrc-2007Q3, pkgsrc-2007Q2-base, pkgsrc-2007Q2, pkgsrc-2007Q1-base, pkgsrc-2007Q1
Changes since 1.4: +129 -265 lines
Diff to previous 1.4 (colored)

Update lang/coq to 8.1

Many changes, among them:
- Many bugs have been fixed (cf coq-bugs web page)
- changed parsing precedence of let/in and fun constructions of Ltac:
  let x := t in e1; e2 is now parsed as let x := t in (e1;e2).
- New primitive "external" for communication with tool external to Coq.
- Omega now handles arbitrary precision integers.
- Haskell extraction: types of functions are now printed, better
  unsafeCoerce mechanism, both for hugs and ghc.
- Scheme extraction improved, see
- New notation "exists! x:A, P" for unique existence.
- New library on String and Ascii characters (contributed by L. Thery).
- New library FSets+FMaps of finite sets and maps.
- New library QArith on rational numbers.
- Few improvements in ZArith potentially exceptionally breaking the
  compatibility (useless hypothesys of Zgt_square_simpl and
  Zlt_square_simpl removed; fixed names mentioning letter O instead of
  digit 0; weaken premises in Z_lt_induction).

Revision 1.4 / (download) - annotate - [select for diffs], Wed Jan 17 11:14:46 2007 UTC (16 years, 10 months ago) by tonio
Branch: MAIN
Changes since 1.3: +3 -1 lines
Diff to previous 1.3 (colored)

Add an option "coqide" to enable the gtk2 ide of coq
It's disabled by default, to avoid too much dependancies

Revision 1.3 / (download) - annotate - [select for diffs], Fri Jan 27 19:22:58 2006 UTC (17 years, 10 months ago) by tonio
Branch: MAIN
CVS Tags: pkgsrc-2006Q4-base, pkgsrc-2006Q4, pkgsrc-2006Q3-base, pkgsrc-2006Q3, pkgsrc-2006Q2-base, pkgsrc-2006Q2, pkgsrc-2006Q1-base, pkgsrc-2006Q1
Changes since 1.2: +82 -81 lines
Diff to previous 1.2 (colored)

Update lang/coq to 8.0pl3

- Coq sources made compatible with ocaml 3.09.0 and lablgtk 2.6.0.
- The search depth argument of auto can be parameterised in the Ltac language
- Added entry constr_may_eval for tactic extensions (new syntax)
- A couple of lemmas of ZArith were renamed: O -> 0
- many bugfixes, for extraction, Ltac, tactics...

Revision 1.2 / (download) - annotate - [select for diffs], Sat Feb 5 11:19:02 2005 UTC (18 years, 10 months ago) by adrianp
Branch: MAIN
CVS Tags: pkgsrc-2005Q4-base, pkgsrc-2005Q4, pkgsrc-2005Q3-base, pkgsrc-2005Q3, pkgsrc-2005Q2-base, pkgsrc-2005Q2, pkgsrc-2005Q1-base, pkgsrc-2005Q1
Changes since 1.1: +287 -29 lines
Diff to previous 1.1 (colored)

- Update of coq from 7.4 to 8.0pl2
- Initial patches supplied by Antoine Reilles, thanks !
- Lots of changes/fixes/updates, see: CHANGES

Revision / (download) - annotate - [select for diffs] (vendor branch), Sat Mar 22 20:21:17 2003 UTC (20 years, 8 months ago) by kristerw
Branch: TNF
CVS Tags: pkgsrc-base, pkgsrc-2004Q4-base, pkgsrc-2004Q4, pkgsrc-2004Q3-base, pkgsrc-2004Q3, pkgsrc-2004Q2-base, pkgsrc-2004Q2, pkgsrc-2004Q1-base, pkgsrc-2004Q1, pkgsrc-2003Q4-base, pkgsrc-2003Q4
Changes since 1.1: +0 -0 lines
Diff to previous 1.1 (colored)

By popular demand, move coq-7.4 from math to lang in order to be consistent
with prior art (e.g. lang/twelf).

    Coq is a Proof Assistant for a Logical Framework known as the
    Calculus of Inductive Constructions. It allows the interactive
    construction of formal proofs, and also the manipulation of
    functional programs consistently with their specifications.

Revision 1.1 / (download) - annotate - [select for diffs], Sat Mar 22 20:21:17 2003 UTC (20 years, 8 months ago) by kristerw
Branch: MAIN

Initial revision

This form allows you to request diff's between any two revisions of a file. You may select a symbolic revision name using the selection box or you may type in a numeric name using the type-in text box.

CVSweb <>