diff options
Diffstat (limited to 'CHANGES')
-rw-r--r-- | CHANGES | 414 |
1 files changed, 330 insertions, 84 deletions
@@ -1,49 +1,317 @@ -Changes from V8.2 to forthcoming V8.2pl1 -======================================== +Changes from V8.2 to V8.3 +========================= -Language and commands +Rewriting tactics + +- Tactic "rewrite" now supports rewriting on ad hoc equalities such as eq_true. +- "Hint Rewrite" now checks that the lemma looks like an equation. +- New tactic "etransitivity". +- Support for heterogeneous equality (JMeq) in "injection" and "discriminate". +- Tactic "subst" now supports heterogeneous equality and equality + proofs that are dependent (use "simple subst" for preserving compatibility). +- Added support for Leibniz-rewriting of dependent hypotheses. +- Renamed "Morphism" into "Proper" and "respect" into "proper_prf" + (possible source of incompatibility). +- New tactic variants "rewrite* by" and "autorewrite*" that rewrite + respectively the first and all matches whose side-conditions are + solved. +- "Require Import Setoid" does not export all of "Morphisms" and + "RelationClasses" anymore (possible source of incompatibility, fixed + by importing "Morphisms" too). +- Support added for using Chung-Kil Hur's Heq library for rewriting over + heterogeneous equality (courtesy of the library's author). +- Tactic "replace" supports matching terms with holes. + +Automation tactics + +- Tactic "intuition" now preserves inner "iff" and "not" (exceptional + source of incompatibilities solvable by redefining "intuition" as + "unfold iff, not in *; intuition", or by using "Set Intuition Unfolding".) +- Tactic "tauto" now proves classical tautologies as soon as classical logic + (i.e. library Classical_Prop or Classical) is loaded. +- Tactic "gappa" has been removed from the Dp plugin. +- Tactic "firstorder" now supports the combination of its "using" and + "with" options. +- New "Hint Resolve ->" (or "<-") for declaring iff's as oriented + hints (wish #2104). +- An inductive type as argument of the "using" option of "auto/eauto/firstorder" + is interpreted as using the collection of its constructors. +- New decision tactic "nsatz" to prove polynomial equations + by computation of Groebner bases. + +Other tactics + +- Tactic "discriminate" now performs intros before trying to discriminate an + hypothesis of the goal (previously it applied intro only if the goal + had the form t1<>t2) (exceptional source of incompatibilities - former + behavior can be obtained by "Unset Discriminate Introduction"). +- Tactic "quote" now supports quotation of arbitrary terms (not just the + goal). +- Tactic "idtac" now displays its "list" arguments. +- New introduction patterns "*" for introducing the next block of dependent + variables and "**" for introducing all quantified variables and hypotheses. +- Pattern Unification for existential variables activated in tactics and + new option "Unset Tactic Evars Pattern Unification" to deactivate it. +- Resolution of canonical structure is now part of the tactic's unification + algorithm. +- New tactic "decide lemma with hyp" for rewriting decidability lemmas + when one knows which side is true. +- Improved support of dependent goals over objects in dependent types for + "destruct" (rare source of incompatibility that can be avoided by unsetting + option "Dependent Propositions Elimination"). +- Tactic "exists", "eexists", "destruct" and "edestruct" supports iteration + using comma-separated arguments. +- Tactic names "case" and "elim" now support clauses "as" and "in" and become + then synonymous of "destruct" and "induction" respectively. +- A new tactic name "exfalso" for the use of 'ex-falso quodlibet' principle. + This tactic is simply a shortcut for "elimtype False". +- Made quantified hypotheses get the name they would have if introduced in + the context (possible but rare source of incompatibilities). +- When applying a component of a conjunctive lemma, "apply in" (and + sequences of "apply in") now leave the side conditions of the lemmas + uniformly after the main goal (possible source of rare incompatibilities). +- In "simpl c" and "change c with d", c can be a pattern. +- Tactic "revert" now preserves let-in's making it the exact inverse of + "intro". +- New tactics "clear dependent H" and "revert dependent H" that + clears (resp. reverts) H and all the hypotheses that depend on H. +- Ltac's pattern-matching now supports matching metavariables that + depend on variables bound upwards in the pattern. -- Fixing Not_found bug in Theorem with. -- Fixing pattern parsing bug #2087. -- Fixing name aliases bug #2085 with modules. -- Fixing checker bug #2065 with -impredicative-set option. -- Complying with 8.1 heuristic when unification returns several solutions. -- Add [Print Opaque Dependencies] command to print the assumptions and - the opaque constants a definition uses. -- Fixing performance issue in Program's type inference when there are - many existentials. -- Fixing bug #2093, using Program does not require to import Program.Tactics - anymore, it will use [idtac] as the default obligation tactic. -- Fix imports when requiring Setoid, to avoid cluttering the context with - internal names (possible source of incompatibility, import Morphisms to fix). -- Fixing bug #2089, Combined Scheme was not treating parameters correctly. -- Fixing Program to use hooks correctly, when called through [Program Coercion] - for example. -- Fixing manual implicit arguments to always work and remove - [Set Manual Implicit Arguments] option (possible source of incompatibility). -- Fixing refine to work with typeclasses. -- Fixing implementation of [Context] to discharge class instances only on definitions - using some of the parameters or the instance itself (possible source of - incompatibility). +Tactic definitions -Tactics +- Ltac definitions support Local option for non-export outside modules. +- Support for parsing non-empty lists with separators in tactic notations. +- New command "Locate Ltac" to get the full name of an Ltac definition. + +Notations + +- Record syntax "{|x=...; y=...|}" now works inside patterns too. +- Abbreviations from non-imported module now invisible at printing time. +- Abbreviations now use implicit arguments and arguments scopes for printing. +- Abbreviations to pure names now strictly behave like the name they refer to + (make redirections of qualified names easier). +- Abbreviations for applied constant now propagate the implicit arguments + and arguments scope of the underlying reference (possible source of + incompatibilities generally solvable by changing such abbreviations from + e.g. "Notation foo' := (foo x)" to "Notation foo' y := (foo x (y:=y))"). +- The "where" clause now supports multiple notations per defined object. +- Recursive notations automatically expand one step on the left for better + factorization; recursion notations inner separators now ensured being tokens. +- Added "Reserved Infix" as a specific shortcut of the corresponding + "Reserved Notation". +- Open/Close Scope command supports Global option in sections. + +Specification language + +- New support for local binders in the syntax of Record/Structure fields. +- Fixpoint/CoFixpoint now support building part or all of bodies using tactics. +- Binders given before ":" in lemmas and in definitions built by tactics are + now automatically introduced (possible source of incompatibility that can + be resolved by invoking "Unset Automatic Introduction"). + +Module system + +- Include Type is now deprecated since Include now accept both modules and + module types. +- Declare ML Module supports Local option. +- The sharing between non-logical object and the management of the + name-space has been improved by the new "Delta-equivalence" on + qualified name. +- The include operator has been extended to high-order structures +- Sequences of Include can be abbreviated via new syntax "<+". +- A module (or module type) can be given several "<:" signatures. +- Interactive proofs are now permitted in module type. Functors can hence + be declared as Module Type and be used later to type themselves. +- A functor application can be prefixed by a "!" to make it ignore any + "Inline" annotation in the type of its argument(s) (for examples of + use of the new features, see libraries Structures and Numbers). + +Extraction + +- When using (Recursive) Extraction Library, the filenames are directly the + Coq ones with new appropriate extensions : we do not force anymore + uncapital first letters for Ocaml and capital ones for Haskell. +- The extraction now tries harder to avoid code transformations that can be + dangerous for the complexity. In particular many eta-expansions at the top + of functions body are now avoided, clever partial applications will likely + be preserved, let-ins are almost always kept, etc. +- Harsh support of module extraction to Haskell and Scheme: module hierarchy + is flattened, module abbreviations and functor applications are expanded, + module types and unapplied functors are discarded. +- Less unsupported situations when extracting modules to Ocaml. In particular + module parameters might be alpha-renamed if a name clash is detected. +- Extract Inductive is now possible toward non-inductive types (e.g. nat => int) +- Extraction Implicit: this new experimental command allows to mark + some arguments of a function or constructor for removed during + extraction, even if these arguments don't fit the usual elimination + principles of extraction, for instance the length n of a vector. +- Files ExtrOcaml*.v in plugins/extraction try to provide a library of common + extraction commands: mapping of basics types toward Ocaml's counterparts, + conversions from/to int and big_int, or even complete mapping of nat,Z,N + to int or big_int, or mapping of ascii to char and string to char list + (in this case recognition of ascii constants is hard-wired in the extraction). -- Fixing correct binding of quantified hypotheses for induction/destruction - when used in Ltac. -- Fixing bad parentheses check in "pose (f binders := ...)" syntax. -- Fixing unbalanced parenthesis in Ltac debug trace printer. -- Fixing missing sort unification check in lemma application (bug #2084). -- Fixing "as" clause of "apply in" that was not working in the general case. -- Fixing eauto not using external hints with no pattern. +Program + +- Streamlined definitions using well-founded recursion and measures so + that they can work on any subset of the arguments directly (uses currying). +- Try to automatically clear structural fixpoint prototypes in + obligations to avoid issues with opacity. +- Use return type clause inference in pattern-matching as in the standard + typing algorithm. +- Support [Local Obligation Tactic] and [Next Obligation with tactic]. +- Use [Show Obligation Tactic] to print the current default tactic. +- [fst] and [snd] have maximal implicit arguments in Program now (possible + source of incompatibility). + +Type classes + +- Declaring axiomatic type class instances in Module Type should be now + done via new command "Declare Instance", while the syntax "Instance" + now always provides a concrete instance, both in and out of Module Type. +- Use [Existing Class foo] to declare foo as a class a posteriori. + [foo] can be an inductive type or a constant definition. No + projections or instances are defined. +- Various bug fixes and improvements: support for defined fields, + anonymous instances, declarations giving terms, better handling of + sections and [Context]. + +Vernacular commands -Tools and development +- New command "Timeout <n> <command>." interprets a command and a timeout + interrupts the interpretation after <n> seconds. +- New command "Compute <expr>." is a shortcut for "Eval vm_compute in <expr>". +- New command "Fail <command>." interprets a command and is successful iff + the command fails on an error (but not an anomaly). Handy for tests and + illustration of wrong commands. +- Most commands referring to constant (e.g. Print or About) now support + referring to the constant by a notation string. +- Made generation of boolean equality automatic for datatypes (use + "Unset Boolean Equality Schemes" for deactivation). +- Made support for automatic generation of case analysis schemes and + congruence schemes available to user (governed by options "Unset + Case Analysis Schemes" and "Unset Congruence Schemes"). +- New command "(Global?) Generalizable [All|No] Variable(s)? ident(s)?" to + declare which identifiers are generalizable in `{} and `() binders. +- New command "Print Opaque Dependencies" to display opaque constants in + addition to all variables, parameters or axioms a theorem or + definition relies on. +- New command "Declare Reduction <id> := <conv_expr>", allowing to write + later "Eval <id> in ...". This command accepts a Local variant. +- Syntax of Implicit Type now supports more than one block of variables of + a given type. +- Command "Canonical Structure" now warns when it has no effects. -- Fixing missing -c option in coq_makefile. -- Temporary hack for coqide.byte "double free or corruption" problem. -- Added support for code development under Bazaar. -- Added support for compilation under Solaris (thanks to Eric Le Lay, #2078). -- Parsing fixes and support for parsing regular comments inline in coqdoc, - using option -parse-comments (suggestions by B. Pierce). +Library + +- Use "standard" Coq names for the properties of eq and identity + (e.g. refl_equal is now eq_refl). Support for compatibility is provided. +- The function Compare_dec.nat_compare is now defined directly, + instead of relying on lt_eq_lt_dec. The earlier version is still + available under the name nat_compare_alt. +- Lemmas in library Relations and Reals have been homogenized a bit. +- The implicit argument of Logic.eq is now maximally inserted, allowing + to simply write "eq" instead of "@eq _" in morphism signatures. +- Wrongly named lemmas (Zlt_gt_succ and Zlt_succ_gt) fixed (potential source + of incompatibilities) +- List library: + - Definitions of list, length and app are now in Init/Datatypes. + Support for compatibility is provided. + - Definition of Permutation is now in Sorting/Permtation.v + - Some other light revisions and extensions (possible source + of incompatibilities solvable by qualifying names accordingly). +- In ListSet, set_map has been fixed (source of incompatibilities if used). +- Sorting library: + - new mergesort of worst-case complexity O(n*ln(n)) made available in + Mergesort.v; + - former notion of permutation up to setoid from Permutation.v is + deprecated and moved to PermutSetoid.v; + - heapsort from Heap.v of worst-case complexity O(n*n) is deprecated; + - new file Sorted.v for some definitions of being sorted. +- Structure library. This new library is meant to contain generic + structures such as types with equalities or orders, either + in Module version (for now) or Type Classes (still to do): + - DecidableType.v and OrderedType.v: initial notions for FSets/FMaps, + left for compatibility but considered as deprecated. + - Equalities.v and Orders.v: evolutions of the previous files, + with fine-grain Module architecture, many variants, use of + Equivalence and other relevant Type Classes notions. + - OrdersTac.v: a generic tactic for solving chains of (in)equalities + over variables. See {Nat,N,Z,P}OrderedType.v for concrete instances. + - GenericMinMax.v: any ordered type can be equipped with min and max. + We derived here all the generic properties of these functions. +- MSets library: an important evolution of the FSets library. + "MSets" stands for Modular (Finite) Sets, by contrast with a forthcoming + library of Class (Finite) Sets contributed by S. Lescuyer which will be + integrated with the next release of Coq. The main features of MSets are: + - The use of Equivalence, Proper and other Type Classes features + easing the handling of setoid equalities. + - The interfaces are now stated in iff-style. Old specifications + are now derived properties. + - The compare functions are now pure, and return a "comparison" value. + Thanks to the CompSpec inductive type, reasoning on them remains easy. + - Sets structures requiring invariants (i.e. sorted lists) are + built first as "Raw" sets (pure objects and separate proofs) and + attached with their proofs thanks to a generic functor. "Raw" sets + have now a proper interface and can be manipulated directly. + Note: No Maps yet in MSets. The FSets library is still provided + for compatibility, but will probably be considered as deprecated in the + next release of Coq. +- Numbers library: + - The abstract layer (NatInt, Natural/Abstract, Integer/Abstract) has + been simplified and enhance thanks to new features of the module + system such as Include (see above). It has been extended to Euclidean + division (three flavors for integers: Trunc, Floor and Math). + - The arbitrary-large efficient numbers (BigN, BigZ, BigQ) has also + been reworked. They benefit from the abstract layer improvements + (especially for div and mod). Note that some specifications have + slightly changed (compare, div, mod, shift{r,l}). Ring/Field should + work better (true recognition of constants). + +Tools + +- Option -R now supports binding Coq root read-only. +- New coqtop/coqc option -beautify to reformat .v files (usable + e.g. to globally update notations). +- New tool beautify-archive to beautify a full archive of developments. +- New coqtop/coqc option -compat X.Y to simulate the general behavior + of previous versions of Coq (provides e.g. support for 8.2 compatibility). + +Coqdoc + +- List have been revamped. List depth and scope is now determined by + an "offside" whitespace rule. +- Text may be italicized by placing it in _underscores_. +- The "--index <string>" flag changes the filename of the index. +- The "--toc-depth <int>" flag limits the depth of headers which are + included in the table of contents. +- The "--lib-name <string>" flag prints "<string> Foo" instead of + "Library Foo" where library titles are called for. The + "--no-lib-name" flag eliminates the extra title. +- New option "--parse-comments" to allow parsing of regular "(* *)" + comments. +- New option "--plain-comments" to disable interpretation inside comments. +- New option "--interpolate" to try and typeset identifiers in Coq escapings + using the available globalization information. +- New option "--external url root" to refer to external libraries. +- Links to section variables and notations now supported. + +Internal infrastructure + +- To avoid confusion with the repository of user's contributions, + the subdirectory "contrib" has been renamed into "plugins". + On platforms supporting ocaml native dynlink, code located there + is built as loadable plugins for coqtop. +- An experimental build mechanism via ocamlbuild is provided. + From the top of the archive, run ./configure as usual, and + then ./build. Feedback about this build mechanism is most welcome. + Compiling Coq on platforms such as Windows might be simpler + this way, but this remains to be tested. +- The Makefile system has been simplified and factorized with + the ocamlbuild system. In particular "make" takes advantage + of .mllib files for building .cma/.cmxa. The .vo files to + compile are now listed in several vo.itarget files. Changes from V8.1 to V8.2 ========================= @@ -60,7 +328,6 @@ Language 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 @@ -75,10 +342,6 @@ Language 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 @@ -117,14 +380,6 @@ Vernacular commands - "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. @@ -231,6 +486,7 @@ Libraries contribution repository (contribution CoC_History). New lemmas about transitive closure added and some bound variables renamed (exceptional risk of incompatibilities). +- Syntax for binders in terms (e.g. for "exists") supports anonymous names. Notations, coercions, implicit arguments and type inference @@ -238,13 +494,13 @@ Notations, coercions, implicit arguments and type inference 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 - declarations. +- Improved inference of implicit arguments. - 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 modifier of "Implicit Arguments" to enrich the set of implicit arguments. - New options Global and Local to "Implicit Arguments" for section surviving or non export outside module. - Level "constr" moved from 9 to 8. @@ -260,8 +516,6 @@ Tactic Language (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 .." @@ -286,15 +540,11 @@ Tactic Language 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 - documented. Tactics - 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". @@ -389,6 +639,9 @@ Program programming (id, apply, flip...) - More robust obligation handling, dependent pattern-matching and well-founded definitions. +- New syntax " dest term as pat in term " for destructing objects using + an irrefutable pattern while keeping equalities (use this instead of + "let" in Programs). - 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 @@ -407,8 +660,8 @@ 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 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 @@ -432,9 +685,10 @@ Setoid rewriting 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. + - One needs to use [Typeclasses unfold [cst]] if [cst] is used + as an abbreviation hiding products in types of morphisms, + e.g. if ones redefines [relation] and declares morphisms + whose type mentions [relation]. - The [setoid_rewrite]'s semantics change when rewriting with a lemma: it can rewrite two different instantiations of the lemma @@ -454,12 +708,12 @@ Setoid rewriting 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 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. + is always the same: first the new goal, then the conditions. - New standard library modules Classes.Morphisms declares standard morphisms on refl/sym/trans relations. @@ -512,19 +766,11 @@ Tools - 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". - -coqdoc - 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. + supported, which makes typesetting trivial in the generated documentation. + Support for hyperlinking and indexing developments in the tex output + has been implemented as well. Miscellaneous @@ -1061,7 +1307,7 @@ Tactics - Clear now fails when trying to remove a local definition used by a constant appearing in the current goal -Extraction (See details in contrib/extraction/CHANGES) +Extraction (See details in plugins/extraction/CHANGES) - The old commands: (Recursive) Extraction Module M. are now: (Recursive) Extraction Library M. @@ -1201,7 +1447,7 @@ Tactics - Unfold expects a correct evaluable argument - Clear expects existing hypotheses -Extraction (See details in contrib/extraction/CHANGES and README): +Extraction (See details in plugins/extraction/CHANGES and README): - An experimental Scheme extraction is provided. - Concerning Ocaml, extracted code is now ensured to always type-check, @@ -1316,7 +1562,7 @@ Bugs - Known bugs related to Inversion and let-in's fixed - Bug unexpected Delta with let-in now fixed -Extraction (details in contrib/extraction/CHANGES or documentation) +Extraction (details in plugins/extraction/CHANGES or documentation) - Signatures of extracted terms are now mostly expunged from dummy arguments. - Haskell extraction is now operational (tested & debugged). @@ -1324,7 +1570,7 @@ Extraction (details in contrib/extraction/CHANGES or documentation) Standard library - Some additions in [ZArith]: three files (Zcomplements.v, Zpower.v - and Zlogarithms.v) moved from contrib/omega in order to be more + and Zlogarithms.v) moved from plugins/omega in order to be more visible, one Zsgn function, more induction principles (Wf_Z.v and tail of Zcomplements.v), one more general Euclid theorem - Peano_dec.v and Compare_dec.v now part of Arith.v @@ -1387,7 +1633,7 @@ Tactics - Slight improvement in naming strategy for NewInduction/NewDestruct - Intuition/Tauto do not perform useless unfolding and work up to conversion -Extraction (details in contrib/extraction/CHANGES or documentation) +Extraction (details in plugins/extraction/CHANGES or documentation) - Syntax changes: there are no more options inside the extraction commands. New commands for customization and options have been introduced instead. |