diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 117 |
1 files changed, 85 insertions, 32 deletions
@@ -13,13 +13,14 @@ Language arguments in terms. - Sort of Record/Structure, Inductive and CoInductive defaults to Type if omitted. -- Record/Structure now usable for defining coinductive types - (e.g. "Record stream := { hd : nat; tl : stream }.") +- 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 statements. - 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). (TODO: Say more!) + 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 @@ -27,6 +28,10 @@ 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 @@ -55,12 +60,28 @@ Vernacular commands 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. -Libraries (DOC TO CHECK) +Libraries - Several parts of the libraries are now in Type, in particular FSets, SetoidList, ListSet, Sorting, Zmisc. This may induce a few @@ -93,6 +114,11 @@ Libraries (DOC TO CHECK) 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. @@ -155,7 +181,9 @@ Libraries (DOC TO CHECK) - 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). + 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 @@ -163,17 +191,16 @@ 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. +- Improved inference of implicit arguments, now working inside record + declarations. - 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. - (DOC TODO?) - New options Global and Local to "Implicit Arguments" for section surviving or non export outside module. -- Level "constr" moved from 9 to 8. (DOC TODO?) +- 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 @@ -184,6 +211,8 @@ 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). @@ -192,7 +221,7 @@ Tactic Language 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. (DOC TODO) + 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 @@ -206,12 +235,19 @@ Tactic Language "let ... in ..." into a lazy one. - Patterns for hypotheses types in "match goal" are now interpreted in type_scope. +- 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 + documented. Tactics - New tactics "apply -> term", "apply <- term", "apply -> term in - ident", "apply <- term in ident" for applying equivalences (iff). (DOC TODO) + 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". @@ -230,6 +266,7 @@ Tactics 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: @@ -238,7 +275,7 @@ Tactics 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": (DOC TODO) +- 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". @@ -258,21 +295,21 @@ Tactics - 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. -- Tactic "apply" 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); - version of apply that does not unfold is renamed into "simple apply" - (usable for compatibility or for automation). -- Tactic "apply" 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. +- 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 hypothesis. + 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 @@ -295,6 +332,8 @@ Tactics occurrences of a term. - Tactic "pose proof" supports name overwriting in case of specialization of an hypothesis. +- Semi-decision tactic "jp" for first-order intuitionistic logic moved to user + contributions (subsumed by "firstorder"). Program @@ -321,8 +360,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 @@ -346,10 +385,9 @@ Setoid rewriting Their introduction may break existing scripts that defined them as notations with different levels. - - 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]. + - 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 @@ -369,12 +407,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 always the same: first the new goal, then the 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. @@ -406,6 +444,9 @@ Extraction possible if several branches are identical. For instance, functions corresponding to decidability of equalities are now linear instead of quadratic. +- A new instruction Extraction Blacklist id1 .. idn allows to prevent filename + conflits with existing code, for instance when extracting module List + to Ocaml. CoqIDE @@ -425,6 +466,19 @@ Tools - 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. + Miscellaneous - Coq installation provides enough files so that Ocaml's extensions need not @@ -572,7 +626,7 @@ Tactics juste a simple hypothesis name. For instance: rewrite H in H1,H2 |- * means rewrite H in H1; rewrite H in H2; rewrite H rewrite H in * |- will do try rewrite H in Hi for all hypothesis Hi <> H. -- Added "dependent rewrite term" and "dependent rewrite term in hyp" (doc TODO) +- Added "dependent rewrite term" and "dependent rewrite term in hyp". - Added "autorewrite with ... in hyp [using ...]". - Tactic "replace" now accepts a "by" tactic clause. - Added "clear - id" to clear all hypotheses except the ones depending in id. @@ -851,8 +905,7 @@ Vernacular commands - "Declare ML Module" now allows to import .cma files. This avoids to use a bunch of "Declare ML Module" statements when using several ML files. -- "Set Printing Width n" added, allows to change the size of width printing - (TODO : doc). +- "Set Printing Width n" added, allows to change the size of width printing. - "Implicit Variables Type x,y:t" (new syntax: "Implicit Types x y:t") assigns default types for binding variables. - Declarations of Hints and Notation now accept a "Local" flag not to |