From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 8 Aug 2008 13:18:42 +0200 Subject: Imported Upstream version 8.2~beta4+dfsg --- CHANGES | 29 +++++++++++++++++++++++++---- 1 file changed, 25 insertions(+), 4 deletions(-) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index 675db3f1..01a81554 100644 --- a/CHANGES +++ b/CHANGES @@ -21,10 +21,16 @@ Language - Several evolutions of the module system (handling of module aliases, functorial module types, an Include feature, etc). (TODO: Say more!) - 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]. Vernacular commands -- Added option Global to "Arguments Scope" for section surviving. (DOC TODO) +- 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 @@ -51,6 +57,8 @@ Vernacular commands that should be expanded first. - 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). Libraries (DOC TO CHECK) @@ -146,6 +154,8 @@ Libraries (DOC TO CHECK) 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). Notations, coercions, implicit arguments and type inference @@ -174,6 +184,8 @@ Tactic Language - Second-order pattern-matching now working in Ltac "match" clauses (syntax for second-order unification variable is "@?X"). +- (?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 .." @@ -194,6 +206,7 @@ Tactic Language "let ... in ..." into a lazy one. - Patterns for hypotheses types in "match goal" are now interpreted in type_scope. +- New printing of Ltac call trace for better debugging. Tactics @@ -239,6 +252,9 @@ Tactics * "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. @@ -250,6 +266,7 @@ Tactics - 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. +- 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 @@ -268,6 +285,7 @@ Tactics 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 @@ -275,6 +293,8 @@ Tactics 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 + hypothesis. Program @@ -283,13 +303,11 @@ 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 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 @@ -403,6 +421,8 @@ CoqIDE Tools - 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. Miscellaneous @@ -413,6 +433,7 @@ Miscellaneous - 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 Changes from V8.1gamma to V8.1 ============================== -- cgit v1.2.3