path: root/CHANGES

Changes from V6.3.1 and V7.0 to V7.1
------------------------------------

Notes:
- items followed by (**) are important sources of incompatibilities
- items followed by (*) may exceptionally be sources of incompatibilities
- items followed by (+) have been introduced in version 7.0


Language

- New construction for local definitions (Let-In) with syntax [x:=u]t (+)
- New reduction flags Zeta and Evar in Eval Compute, for inlining of
  local definitions and instantiation of existential variables
- Delta reduction flag does not perform Zeta and Evar reduction any more (*)
- New visibility discipline for Remark, Fact and Local: Remark's and
  Fact's now survive at the end of section, but are only accessible using a
  qualified names as soon as their strength expires; Local's disappear and
  are moved into local definitions for each construction persistent at
  section closing
- Constants declared as opaque (using Qed) can no longer become
  transparent (a constant intended to be alternatively opaque and
  transparent must be declared as transparent (using Defined));
  a risk exists (until next Coq versin) that Simpl reduces opaque constants (*)
- Local definitions allowed in Record (aka record à la Randy Pollack)
- The names of variables for Record projections _and_ for induction principles
  (e.g. sum_ind) is now based on the first letter of their type (main
  source of incompatibility) (**)(+)
- Most typing errors have now a precise location in the source (+)
- Cases no longer infers aliases by looking at dependencies (*)(+)
- Slightly different mechanism to solve "?" (*)(+)
- More arguments may be considered implicits at section closing (*)(+)
- A redundant clause in Cases is now an error (*)
- Known Coercion bugs fixed
- Cases predicate inference bug fixed
- Known dependent Cases predicate bugs fixed
- Bug with identifiers ended by a number greater than 2^30 fixed (+)

Language : long names

- Each construction has a unique absolute names built from a base
  name, the name of the module in which they are defined (Top if in
  coqtop), and possibly an arbitrary long sequence of directory (e.g.
  "Coq.Lists.PolyList.flat_map" where "Coq" means that "flat_map" is part
  of Coq standard library, "Lists" means it is defined in the Lists
  library and "PolyList" means it is in the file Polylist) (+)
- Constructions can be referred by their base name, or, in case of
  conflict, by a "qualified" name, where the base name is prefixed
  by the module name (and possibly by a directory name, and so
  on). A fully qualified name is an absolute name which always refer
  to the the construction it denotes (to preserve the visibility of
  all constructions, no conflict is allowed for an absolute name) (+)
- Long names are available for modules with the possibility of using
  the directory name as a component of the module full name (with
  option -R to coqtop and coqc, or command Add LoadPath) (+)
- Improved conflict resolution strategy (the Unix PATH model),
  allowing more constructions to be referred just by their base name



New tactics

- New set of tactics to deal with types equipped with specific
  equalities (aka Setoïds, e.g. nat equipped with eq_nat) [by C. Renard]
- New tactic Assert, similar to Cut but expected to be more user-friendly
- New tactic NewDestruct and NewInduction intended to replace Elim
  and Induction, Case and Destruct in a more user-friendly way (see
  restrictions in the reference manual)
- New tactic ROmega: an experimental alternative (based on reflexion) to Omega
  [by P. Crégut]
- New tactic language Ltac (see reference manual) (+)
- New versions of Tauto and Intuition, fully rewritten in the new Ltac
  language; they run faster and produce more compact proofs; Tauto is
  fully compatible but, in exchange of a better uniformity, Intuition
  is slightly weaker (then used Tauto instead) (**)(+)
- New tactic Field to decide equalities on commutative fields (as a
  special case, it works on real numbers) (+)
- New tactic Fourier to solve linear inequalities on reals numbers
  [by L. Pottier] (+)
- New tactics dedicated to real numbers: DiscrR, SplitRmult, SplitAbsolu (+)


Changes in tactics

- Reduction tactics in local definitions apply only to the body
- New syntax of the form "Compute in Type of H." to require a reduction on
  the types of local definitions
- Inversion, Injection, Discriminate, ... apply also on the
  quantified premises of a goal (using the "Intros until" syntax)
- Decompose has been fixed but hypotheses may get different names (*)(+)
- Tauto now manages uniformly hypotheses and conclusions of the form
  "t=t" which all are considered equivalent to "True". Especially,
  Tauto now solves goals of the form "H : ~ t = t |- A".
- The "Let" tactic has been renamed "LetTac" and is now based on the
  primitive "let-in" (+)
- Elim can no longer be used with an elimination schema different from
  the one defined at definition time of the inductive type. To overload
  an elimination schema, use "Elim <hyp> with <name of the new schema>" (*)(+)
- Simpl no longer unfolds the recursive calls of a mutually defined 
  fixpoint (*)(+)
- Intro now fails if the hypothesis name already exists (*)(+)
- "Require Prolog" is no longer needed (i.e. it is available by default) (*)(+)
- Unfold now fails on a non unfoldable identifier (*)(+)
- Unfold also applies on definitions of the local context
- AutoRewrite now deals only with the main goal and it is the purpose of
  Hint Rewrite to deal with generated subgoals (+)
- Redundant or incompatible instantiations in Apply ... with ... are now
  correctly managed (+)


Efficiency

- Excessive memory uses specific to V7.0 fixed
- Sizes of .vo files vary a lot compared to V6.3 (from -30% to +300%
  depending on the developments)


Parsing and grammar extension

- Only identifiers starting with "_" or a letter, and followed by letters,
  digits, "_" or "'" are allowed (e.g. "$" and "@" are no longer allowed) (*)
- Un lieur multiple comme (a:A)(a,b:(P a))(Q a), n'est plus compris comme
  (a:A)(a0:(P a))(b:(P a))(Q a0), mais comme 
  (a:A)(a0:(P a))(b:(P a0))(Q a0)  (*)(+)
- More constraints when writing ast 
  - "{...}" and the macros $LIST, $VAR, etc. now expect a metavariable
    (an identifier starting with $) (*)
  - identifiers should starts with a letter or "_" and be followed
     by letters, digits, "_" or "'" (other caracters are still
     supported but it is not advised to use them) (*)(+)
- Entry "command" in "Grammar" and quotations (<<...>> stuff) is
  renamed "constr" as in "Syntax" (+)
- New syntax "[" sentence_1 ... sentence_n"]." to group sentences (useful
  for Time and to write grammar rules abbreviating several commands) (+)
- The default parser for actions in the grammar rules (and for
  patterns in the pretty-printing rules) is now the one associated to
  the grammar (i.e. vernac, tactic or constr); no need then for
  quotations as in <:vernac:<...>>; to return an "ast", the grammar
  must be explicity typed with tag ": ast" or ": ast list", or if a
  syntax rule, by using <<...>> in the patterns (expression inside
  these angle brackets are parsed as "ast"); for grammars other than
  vernac, tactic or constr, you may explicitly type the action with
  tags ": constr", ": tactic", or ":vernac" (**)(+)
- Interpretation of names in Grammar rule is now based on long names,
  which allows to avoid problems (or sometimes tricks;) related to
  overloaded names (+)
- A dedicated syntax has been introduced for Reals (e.g ``3+1/x``) (+)
- Pretty-printing of Infix notations fixed. (+)


New commands

- New command to manually set implicits arguments (+)
  - "Implicits ident." to activate the implicit arguments mode just for ident
  - "Implicits ident [num1 num2 ...]." to explicitly give which
    arguments have to be considered as implicit
- New SearchPattern/SearchRewrite (by Yves Bertot) (+)
- New command "Debug on"/"Debug off" to activate/deactivate the tactic
  language debuger (+)
- New command to map physical paths to logical paths (+)
  - Add LoadPath physical_dir as logical_dir
  - Add Rec LoadPath physical_dir as logical_dir


Changes in existing commands

- Generalization of the usage of qualified identifiers in tactics
  and commands about globals, e.g. Decompose, Eval Delta; 
  Hints Unfold, Transparent, Require
- Require synchronous with Reset; Require's scope stops at Section ending (*)
- For a module indirectly loaded by a "Require" but not exported,
  the command "Import module" turns the constructions defined in the
  module accessible by their short name, and activates the Grammar,
  Syntax, Hint, ... declared in the module (+)
- The scope of the "Search" command can be restricted to some modules (+)
- Final dot in command (full stop) must be followed by a space
  (newline, tablation or whitespace) (+)
- Slight restriction of the syntax for Cbv Delta: if present, option [-myconst]
  must immediately follow the Delta keyword (*)(+)
- SearchIsos currently not suppported
- Add ML Path is now implied by Add LoadPath (+)
- New names for the following commands (+)

  AddPath -> Add LoadPath
  Print LoadPath -> Print LoadPath
  DelPath -> Remove LoadPath
  AddRecPath -> Add Rec LoadPath
  Print Path -> Print Coercion Paths

  Implicit Arguments On -> Set Implicit Arguments
  Implicit Arguments Off -> Unset Implicit Arguments

  Begin Silent -> Set Silent
  End Silent -> Unset Silent.


Tools

- coqtop (+)
  - Two executables: coqtop.byte and coqtop.opt (if supported by the platform)
  - coqtop is a link to the more efficient executable (coqtop.opt if present)
  - option -full is obsolete (+)
- do_Makefile renamed into coq_makefile (+)
- New option -R to coqtop and coqc to map a physical directory to a logical
  one (+)
- coqc no longer needs to create a temporary file
- No more warning if no initialization file .coqrc exists


Extraction

- New algorithm for extraction able to deal with "Type" (+)


Standard library

- New library on maps on integers (IntMap, contributed by Jean Goubault)
- New lemmas about integer numbers [ZArith]
- New lemmas about [Reals] (+)
- Exc/Error/Value renamed into Option/Some/None (*)


New user contributions

- Constructive complex analysis and the Fundamental Theorem of Algebra [FTA]
  (Herman Geuvers, Freek Wiedijk, Jan Zwanenburg, Randy Pollack,
   Henk Barendregt, Nijmegen)
- A new axiomatization of ZFC set theory [Functions_in_ZFC]
  (C. Simpson, Sophia-Antipolis)
- Basic notions of graph theory [GRAPHS-BASICS] (Jean Duprat, Lyon)
- A library for floating-point numbers [Float] (Laurent Théry, Sylvie Boldo,
  Sophia-Antipolis)
- Formalisation of CTL and TCTL temporal logic [CtlTctl] (Carlos
  Daniel Luna,Montevideo)
- Specification and verification of the Railroad Crossing Problem
  in CTL and TCTL [RailroadCrossing] (Carlos Daniel Luna,Montevideo)
- P-automaton and the ABR algorithm [PAutomata]
  (Christine Paulin, Emmanuel Freund, Orsay)
- Semantics of a subset of the C language [MiniC] 
  (Eduardo Giménez, Emmanuel Ledinot, Suresnes) 
- Correctness proofs of the following imperative algorithms:
  Bresenham line drawing algorithm [Bresenham], Marché's minimal edition
  distance algorithm [Diff] (Jean-Christophe Filliâtre, Orsay)
- Correctness proofs of Buchberger's algorithm [Buchberger] and RSA
  cryptographic algorithm [Rsa] (Laurent Théry, Sophia-Antipolis)
- Correctness proof of Stalmarck tautology checker algorithm
  [Stalmarck] (Laurent Théry, Pierre Letouzey, Sophia-Antipolis)