diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 475 |
1 files changed, 352 insertions, 123 deletions
@@ -1,132 +1,355 @@ -Changes from V8.4pl3 to V8.4pl4 -=============================== - -WARNING: -The current logic of Coq is now known to be inconsistent with - Axiom prop_extensionality : forall A B:Prop, (A <-> B) -> A = B. -For more details, see: - https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq/coq.git;a=blob_plain;f=test-suite/failure/subterm2.v;hb=HEAD -or - https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq/coq.git;a=blob_plain;f=test-suite/failure/subterm3.v;hb=HEAD - -Kernel - -- Bug #3211: unsound check of elimination sort. -- Fix guard condition for nested cofixpoints. -- Bug #3243: Univ constraints of module subtyping were not propagated. - -Tactics - -- A new option "Set Stable Omega" ensures that repeated identical calls - to omega will produce identical proof terms. This option is off by default - for maximal compatibility, but should be pretty safe to activate. -- The interpretation of the open_constr tactic argument was erroneously - firing type classes resolution in some corner cases. This has been - fixed. The tactic argument type open_constr_wTC is provided for retro - compatibility purposes. -- Fixing bug #3228 (fixing precedence of ltac variables over variables in - env) introduces rare and justified tactic failure. - -Bug fixes - -- Solved bugs: - #3260, #2697, #3037, #3262, #2900, #3131, #3238, #3204, #1758, #1039, - #3144 -- micromega: solved an ambiguous symbol resolution. -- Coq always uses / as separator between directories on all platforms. -- remove trailing '\r' from file names returned by coqtop. -- bug correction in proving inversion principles for Function. -- ocamlbuild: minor fixes related to camlp4 and cross-compilation. - -Changes from V8.4pl2 to V8.4pl3 -=============================== - -Ide_slave XML interface - -- 20120712, 20130419 : Invalidated protocol versions -- From 20130419 extra datastructure : union - (Inl "" = <union val="in_l"><string></string></union>, - Inr _ = <union val="in_r">...) -- 20130419~1 : new toplevel entry : message, not send by coptop v8.4 and not - handle by coqide v8.4. A message has a level and a content (of string). - Message levels are Debug of string, Info, Notice, Warning and Error. -- 20130425 : - * new toplevel entry : feedback, once again not send by coqtop v8.4 and not - handle by coqide v8.4. A feedback gives the id of the sentence it provides info - about and a content. Feedback contents are Processed, AddedAxiom and - GlobRef of Util.loc * string * string * string * string - * <call val="interp"> must provide an attribute id of type int. It is OK in - coqtop v8.4 to alwais send <call val="interp" id="0"> - -Bug fixes - -- Solved bugs: - #2230 #2837 #2846 #2987 #3003 #3001 #3013 #3023 #3025 #3036 #3118 #3169 - #(3150, 3151, 3152, 3153) -- Fixing a significant efficiency leak in the code of the field tactic. -- Fix caching of local hint database in typeclasses eauto which could - miss some hypotheses. -- Fix automatic solving of obligation in program, which was not trying - to solve obligations that had no undefined dependencies left. - -Changes from V8.4pl1 to V8.4pl2 -=============================== - -Bug fixes - -- Solved bugs : - #2466 #2629 #2668 #2750 #2839 #2869 #2954 #2955 #2959 #2962 #2966 #2967 - #2969 #2970 #2975 #2976 #2977 #2978 #2981 #2983 #2995 #3000 #3004 #3008 -- Partially fixed bugs : #2830 #2949 -- Coqtop should now react more reliably when receiving interrupt signals: - all the "try...with" constructs have been protected against undue - handling of the Sys.Break exception. +Changes from V8.4 to V8.5beta1 +============================== -Coqide +Logic -- The Windows-specific code handling the interrupt button of Coqide - had to be reworked (cf. bug #2869). Now, in Win32 this button does - not target a specific coqtop client, but instead sends a Ctrl-C to - any process sharing its console with Coqide. To avoid awkward - effects, it is recommended to launch Coqide via its icon, its menu, - or in a dedicated console window. +- Primitive projections for records allow for a compact representation + of projections, without parameters and avoid the behavior of defined + projections that can unfold to a case expression. To turn the use of + native projections on, use [Set Primitive Projections]. Record, + Class and Structure types defined while this option is set will be + defined with primitive projections instead of the usual encoding as + a case expression. For compatibility, when p is a primitive + projection, @p can be used to refer to the projection with explicit + parameters, i.e. [@p] is definitionally equal to [λ params r. r.(p)]. + Records with primitive projections have eta-conversion, the + canonical form being [mkR pars (p1 t) ... (pn t)]. + +- New universe polymorphism (see reference manual) +- New option -type-in-type to collapse the universe hierarchy (this makes the + logic inconsistent). +- The guard condition for fixpoints is now a bit stricter. Propagation of +subterm value through pattern matching is restricted according to the return +predicate. Restores compatibility of Coq's logic with the propositional +extensionality axiom. May create incompatibilities in recursive programs heavily +using dependent types. -Extraction +Vernacular commands -- The option Extraction AccessOpaque is now set by default, - restoring compatibility of older versions of Coq (cf bug #2952). +- A command "Variant" allows to define non-recursive variant types. +- The command "Record foo ..." does not generate induction principles + (foo_rect, foo_rec, foo_ind) anymore by default (feature wish + #2693). The command "Variant foo ..." does not either. A flag + "Set/Unset Nonrecursive Elimination Schemes" allows changing this. + The tactic "induction" on a "Record" or a "Variant" is now actually + doing "destruct". +- The "Open Scope" command can now be given also a delimiter (e.g. Z). +- The "Definition" command now allows the "Local" modifier, allowing + for non-importable definitions. The same goes for "Axiom" and "Parameter". +- Section-specific commands such as "Let" (resp. "Variable", "Hypothesis") used + out of a section now behave like the corresponding "Local" command, i.e. + "Local Definition" (resp. "Local Parameter", "Local Axiom"). (potential source + of rare incompatibilities). +- The "Let" command can now define local (co)fixpoints. +- Command "Search" has been renamed into "SearchHead". The command + name "Search" now behaves like former "SearchAbout". The latter name + is deprecated. +- "Search" "About" "SearchHead" "SearchRewrite" and "SearchPattern" + now search for hypothesis (of the current goal by default) first. + They now also support the goal selector prefix to specify another + goal to search: e.g. "n:Search id". This is also true for + SearchAbout although it is deprecated. +- The coq/user-contrib directory and the XDG directories are no longer + recursively added to the load path, so files from installed libraries + now need to be fully qualified for the "Require" command to find them. + The tools/update-require script can be used to convert a development. +- A new Print Strategies command allows visualizing the opacity status + of the whole engine. +- The "Locate" command now searches through all sorts of qualified namespaces of + Coq: terms, modules, tactics, etc. The old behavior of the command can be + retrieved using the "Locate Term" command. +- New "Derive" command to help writing program by derivation. +- "Undo" undoes any command, not just tactics. +- New "Refine Instance Mode" option that allows to deactivate the generation of + obligations in incomplete typeclass instances, raising an error instead. +- "Collection" command to name sets of section hypotheses. Named collections + can be used in the syntax of "Proof using" to assert with section variables + are used in a proof. +- The "Optimize Proof" command can be placed in the middle of a proof to + force the compaction the data structure used to represent the ongoing + proof (evar map). This may result in a lower memory footprint and speed up + the execution of the following tactics. +- "Optimize Heap" command to tell the OCaml runtime to performa a major + garbage collection step and heap compaction. + +Specification Language + +- Slight changes in unification error messages. +- Added a syntax $(...)$ that allows putting tactics in terms (may + break user notations using "$(", fixable by inserting a space or + rewriting the notation). +- Constants in pattern-matching branches now respect the same rules regarding + implicit arguments than in applicative position. The old behavior can be + recovered by the command "Set Asymmetric Patterns". (possible source of + incompatibilities) +- Type inference algorithm now granting opacity of constants. This might also + affect behavior of tactics (source of incompatibilities, solvable by + re-declaring transparent constants which were set opaque). +- Existential variables are now referred to by an identifier and the + relevant part of their instance is displayed by default. They can be + reparsed. The naming policy is yet unstable and subject to changes + in future releases. -Changes from V8.4 to V8.4pl1 -============================ +Tactics -Bug fixes +- New tactic engine allowing dependent subgoals, fully backtracking + (also known as multiple success) tactics, as well as tactics which + can consider multiple goals together. In the new tactic engine, + instantiation information of existential variables is always + propagated to tactics, removing the need to manually use the + "instantiate" tactics to mark propagation points. + * New tactical (a+b) insert a backtracking point. When (a+b);c fails + during the execution of c, it can backtrack and try b instead of a. + * New tactical (once a) removes all the backtracking point from a + (i.e. it selects the first success of a). + * Tactic "constructor" is now fully backtracking, thus deprecating + the need of the undocumented "constructor <tac>" syntax which is + now equivalent to "once (constructor; tac)". (potential source of + rare incompatibilities). + * New "multimatch" variant of "match" tactic which backtracks to + new branches in case of a later failure. The "match" tactic is + equivalent to "once multimatch". + * New selector all: to qualify a tactic allows applying a tactic to + all the focused goal, instead of just the first one as is the + default. + * A corresponding new option Set Default Goal Selector "all" makes + the tactics in scripts be applied to all the focused goal by default + * New selector par: to qualify a tactic allows applying a (terminating) + tactic to all the focused goal in parallel. The number of worker can + be selected with -async-proofs-tac-j and also limited using the + coqworkmgr utility. + * New tactics "revgoals", "cycle" and "swap" to reorder goals. + * The semantics of recursive tactics (introduced with Ltac t := + ... or let rec t := ... in ...) changes slightly as t is now + applied to every goal not each goal independently, in particular + it may be applied when no goal are left. This may cause tactics + such as let rec t := constructor;t to loop indefinitely. The + simple fix is to rewrite the recursive calls as follows: let rec t + := constructor;[t..] which recovers the earlier behavior (source + of rare incompatibilities). + * New tactic language feature "numgoals" to count number of goals. + Accompanied by "guard" tactic which fails if a Boolean test does + not pass. + * New tactical "[> ... ]" to apply tactics to individual goals. + * New tactic "gfail" which works like "fail" except it will also + fail if every goal has been solved. + * The refine tactic is changed not to use an ad hoc typing algorithm + to generate subgoals. It also uses the dependent subgoal feature + to generate goals to materialize every existential variable which + is introduced by the refinement (source of incompatibilities). + * A tactic shelve is introduced to manage the subgoals which may be + solved by unification: shelve removes every goal it is applied to + from focus. These goals can later be called back into focus by the + Unshelve command. + * A variant shelve_unifiable only removes those goals which appear + as existential variables in other goals. To emulate the old + refine, use (refine c;shelve_unifiable). This can still cause + incompatibilities in rare occasions. + * New "give_up" tactic to skip over a goal without admitting it. +- Matching using "lazymatch" was fundamentally modified. It now behaves + like "match" (immediate execution of the matching branch) but without + the backtracking mechanism in case of failure. +- New "tryif t then u else v" tactical which executes "u" in case of success + of "t" and "v" in case of failure. +- New conversion tactic "native_compute": evaluates the goal (or an hypothesis) + with a call-by-value strategy, using the OCaml native compiler. Useful on + very intensive computations. +- New "cbn" tactic, a well-behaved simpl. +- Repeated identical calls to omega should now produce identical proof terms. +- Tactics btauto, a reflexive Boolean tautology solver. +- Tactic "tauto" was exceptionally able to destruct other connectives + than the binary connectives "and", "or", "prod", "sum", "iff". This + non-uniform behavior has been fixed (bug #2680) and tauto is + slightly weaker (possible source of incompatibilities). On the + opposite side, new tactic "dtauto" is able to destruct any + record-like inductive types, superseding the old version of "tauto". +- Similarly, "intuition" has been made more uniform and, where it now + fails, "dintuition" can be used. (possible source of incompatibilities) +- Tactic notations can now be defined locally to a module (use "Local" prefix). +- Tactic "red" now reduces head beta-iota redexes (potential source of + rare incompatibilities). +- Tactic "hnf" now reduces inner beta-iota redexes + (potential source of rare incompatibilities). +- Tactic "intro H" now reduces beta-iota redexes if these hide a product + (potential source of rare incompatibilities). +- In Ltac matching on patterns of the form "_ pat1 ... patn" now + behaves like if matching on "?X pat1 ... patn", i.e. accepting "_" + to be instantiated by an applicative term (experimental at this + stage, potential source of incompatibilities). +- In Ltac matching on goal, types of hypotheses are now interpreted in + the %type scope (possible source of incompatibilities). +- "change ... in ..." and "simpl ... in ..." now properly consider nested + occurrences (possible source of incompatibilities since this alters + the numbering of occurrences), but do not support nested occurrences. +- Tactics simpl, vm_compute and native_compute can be given a notation string + to a constant as argument. +- When given a reference as argument, simpl, vm_compute and + native_compute now strictly interpret it as the head of a pattern + starting with this reference. +- The "change p with c" tactic semantics changed, now type-checking + "c" at each matching occurrence "t" of the pattern "p", and + converting "t" with "c". +- Now "appcontext" and "context" behave the same. The old buggy behavior of + "context" can be retrieved at parse time by setting the + "Tactic Compat Context" flag (possible source of incompatibilities). +- New introduction pattern p/c which applies lemma c on the fly on the + hypothesis under consideration before continuing with introduction pattern p. +- New introduction pattern [= x1 .. xn] applies "injection as [x1 .. xn]" + on the fly if injection is applicable to the hypothesis under consideration + (idea borrowed from Georges Gonthier). Introduction pattern [=] applies + "discriminate" if a discriminable equality. +- Tactic "injection c as ipats" now clears c if c refers to an + hypothesis and moves the resulting equations in the hypotheses + independently of the number of ipats, which has itself to be less + than the number of new hypotheses (possible source of incompatibilities; + former behavior obtainable by "Unset Injection L2R Pattern Order"). +- Tactic "injection" now automatically simplifies subgoals + "existT n p = existT n p'" into "p = p'" when "n" is in an inductive type for + which a decidable equality scheme has been generated with "Scheme Equality" + (possible source of incompatibilities). +- New tactic "rewrite_strat" for generalized rewriting with user-defined + strategies, subsuming autorewrite. +- Injection can now also deduce equality of arguments of sort Prop, by using + the option "Set Injection On Proofs" (disabled by default). Also improved the + error messages. +- Tactic "subst id" now supports id occurring in dependent local definitions. +- Bugs fixed about intro-pattern "*" might lead to some rare incompatibilities. +- New tactical "time" to display time spent executing its argument. +- Tactics referring or using a constant dependent in a section variable which + has been cleared or renamed in the current goal context now fail + (possible source of incompatibilities solvable by avoiding clearing + the relevant hypotheses). +- New construct "uconstr:c" and "type_term c" to build untyped terms. +- Binders in terms defined in Ltac (either "constr" or "uconstr") can + now take their names from identifier defined in Ltac. As a + consequence, a name cannot be used in a binder (constr:(fun x => + ...)) if an Ltac variable of that name already exists and does not + contain an identifier. Source of occasional incompatibilities. +- The "refine" tactic now accepts untyped terms built with "uconstr" + so that terms with holes can be constructed piecewise in Ltac. +- New bullets --, ++, **, ---, +++, ***, ... made available. +- More informative messages when wrong bullet is used. +- bullet suggestion when a subgoal is solved. +- New tactic "enough", symmetric to "assert", but with subgoals + swapped, as a more friendly replacement of "cut". +- In destruct/induction, experimental modifier "!" prefixing the + hypothesis name to tell not erasing the hypothesis. +- Bug fixes in "inversion as" may occasionally lead to incompatibilities. +- Behavior of introduction patterns -> and <- made more uniform + (hypothesis is cleared, rewrite in hypotheses and conclusion and + erasing the variable when rewriting a variable). +- Tactics from plugins are now active only when the corresponding + module is imported (source of incompatibilities, solvable by adding + an "Import", like e.g. "Import Omega"). +- Semantics of destruct/induction has been made more regular in some + edge cases, possibly leading to incompatibilities: + - new goals are now opened when the term does not match a subterm of + the goal and has unresolved holes, while in 8.4 these holes were + turned into existential variables + - when no "at" option is given, the historical semantics which + selects all subterms syntactically identical to the first subterm + matching the given pattern is used + - non-dependent destruct/induction on an hypothesis with premises in + an inductive type with indices is fixed + - residual local definitions are now correctly removed. +- The rename tactic may now replace variables in parallel. -- Solved bugs : - #2851 #2863 #2865 #2893 #2895 #2892 #2905 #2906 #2907 #2917 #2921 - #2930 #2941 #2878 -- Partially fixed bug : #2904 -- Various fixes concerning coq_makefile +Program -Optimizations +- "Solve Obligations using" changed to "Solve Obligations with", + consistent with "Proof with". +- Program Lemma, Definition now respect automatic introduction. +- Add/document "Set Hide Obligations" (to hide obligations in the final + term inside an implicit argument) and "Set Shrink Obligations" (to + minimize dependencies of obligations defined by tactics). -- "Union by rank" optimization for universes contributed by J.H. Jourdan - and G. Sherrer (see union-find-and-coq-universes on gagallium blog). +Notations -Libraries +- The syntax "x -> y" is now declared at level 99. In particular, it has + now a lower priority than "<->": "A -> B <-> C" is now "A -> (B <-> C)" + (possible source of incompatibilities) +- Notations accept term-providing tactics using the $(...)$ syntax. +- "Bind Scope" can no longer bind "Funclass" and "Sortclass". +- A notation can be given a (compat "8.x") annotation, making + it behave like a (only parsing), but flags may active warning + or error when this notation is used. +- More systematic insertion of spaces as a default for printing + notations ("format" still available to override the default). +- In notations, a level modifier referring to a non-existent variable is + now considered an error rather than silently ignored. -- Internal organisation of some modular libraries have slightly changed - due to bug #2904 (GenericMinMax, OrdersTac) -- No more constant "int" in ZArith/Int.v to avoid name clash with OCaml - (cf bug #2878). +Tools -Coqide +- Option -I now only adds directories to the ml path. To add to both + the load path and the ml path, use -I -as. +- Option -Q behaves as -I -as and -R, except that the logical path of + any loaded file has to be fully qualified. +- Option -R no longer adds recursively to the ml path; only the root + directory is added. (Behavior with respect to the load path is + unchanged.) +- Option -nois prevents coq/theories and coq/plugins to be recursively + added to the load path. (Same behavior as with coq/user-contrib.) +- coqdep accepts a -dumpgraph option generating a dot file. +- Makefiles generated through coq_makefile have three new targets "quick" + "checkproof" and "vio2vo", allowing respectively to asynchronously compile + the files without playing the proof scripts, asynchronously checking + that the quickly generated proofs are correct and generating the object + files from the quickly generated proofs. +- The XML plugin was discontinued and removed from the source. +- A new utility called coqworkmgr can be used to limit the number of + concurrent workers started by independent processes, like make and CoqIDE. + This is of interest for users of the par: goal selector. + +Interfaces + +- CoqIDE supports asynchronous edition of the document, ongoing tasks and + errors are reported in the bottom right window. The number of workers + taking care of processing proofs can be selected with -async-proofs-j. +- CoqIDE highlight in yellow "unsafe" commands such as axiom + declarations, and tactics like "admit". +- CoqIDE supports Proof General like key bindings; + to activate the PG mode go to Edit -> Preferences -> Editor. + For the documentation see Help -> Help for PG mode. +- CoqIDE automatically retracts the locked area when one edits the + locked text. +- CoqIDE search and replace got regular expressions power. See the + documentation of OCaml's Str module for the supported syntax. +- Many CoqIDE windows, including the query one, are now detachable to + improve usability on multi screen work stations. + +- Coqtop outputs highlighted syntax. Colors can be configured thanks + to the COQ_COLORS environment variable, and their current state can + be displayed with the -list-tags command line option. + +- Third party user interfaces can install their main loop in $COQLIB/toploop + and call coqtop with the -toploop flag to select it. + +Internal Infrastructure + +- Many reorganizations in the ocaml source files. For instance, + many internal a.s.t. of Coq are now placed in mli files in + a new directory intf/, for instance constrexpr.mli or glob_term.mli. + More details in dev/doc/changes. +- The file states/initial.coq does not exist anymore. Instead, coqtop + initially does a "Require" of Prelude.vo (or nothing when given + the options -noinit or -nois). +- The format of vo files has slightly changed: cf final comments in + checker/cic.mli +- The build system does not produce anymore programs named coqtop.opt + and a symbolic link to coqtop. Instead, coqtop is now directly + an executable compiled with the best OCaml compiler available. + The bytecode program coqtop.byte is still produced. Same for other + utilities. +- Some options of the ./configure script slightly changed: + * The -coqrunbyteflags and its blank-separated argument is replaced + by option -vmbyteflags which expects a comma-separated argument. + * The -coqtoolsbyteflags option is discontinued, see -no-custom instead. -- Improved shutdown of coqtop processes spawned by coqide - (in particular added a missing close_on_exec primitive before forking). -- On windows, launching coqide with the -debug option now produces - a log file in the user's temporary directory. The location of this - log file is displayed in the "About" message. +Miscellaneous +- ML plugins now require a "DECLARE PLUGIN \"foo\"" statement. The "foo" name + must be exactly the name of the ML module that will be loaded through a + "Declare ML \"foo\"" command. Changes from V8.4beta2 to V8.4 ============================== @@ -164,6 +387,9 @@ Libraries - 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. +- List: a couple of lemmas added especially about no-duplication, partitions. +- Init: Removal of the coercions between variants of sigma-types and + subset types (possible source of incompatibility). Changes from V8.4beta to V8.4beta2 ================================== @@ -248,7 +474,7 @@ Tactics 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. +- New tactics constr_eq, is_evar and has_evar for use in Ltac (DOC TODO). - 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 @@ -312,7 +538,7 @@ Vernacular commands - 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. + over a given list of section variables at section ending (DOC TODO). - 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". @@ -329,7 +555,7 @@ Module System 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. + the flag "Set Inline Level ..." to set a level (DOC TODO). - 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 @@ -416,9 +642,10 @@ Extraction - 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". + production of several files (one per coq source) a la "Extraction Library" + (DOC TODO). - New option "Set/Unset Extraction KeepSingleton" for preventing the - extraction to optimize singleton container types. + extraction to optimize singleton container types (DOC TODO). - 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). @@ -430,7 +657,8 @@ CoqIDE (cf button "Restart Coq", ex-"Go to Start"). For allowing such interrupts, the Windows version of coqide now requires Windows >= XP SP1. -- The communication between CoqIDE and Coqtop is now done via a dialect of XML. +- The communication between CoqIDE and Coqtop is now done via a dialect + of XML (DOC TODO). - 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 @@ -538,6 +766,9 @@ Other tactics 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. +- New experimental option "Set Standard Proposition Elimination Names" + so that case analysis or induction on schemes in Type containing + propositions now produces "H"-based names. Tactic definitions @@ -2536,5 +2767,3 @@ New user contributions - Correctness proof of Stalmarck tautology checker algorithm [Stalmarck] (Laurent Théry, Pierre Letouzey, Sophia-Antipolis) - - LocalWords: recommended |