Project Filelist for CoqFiniteGroups
File Release Notes and Changelog
Release Name: 1.3pl2
Change Log
While the .v files are the ones part of 1.3pl1, the Coq plugin received many fixes and is fully compatible with the .v files that will be released as part of Ssreflect 1.4. Changes: - Views in intro patterns work even if alternated with regular intro patterns, like in "case=> a /v b". - "set (f:= fun _:Set =>0)" does not discard the anonymous abstraction anymore. - "elim" correctly handles delta expansions and let-ins in the eliminator's type. - "elim"'s predicate is typechecked to avoid generating an ill-typed goal. - Different error messages for "dependent rewrite" errors and "indetermined RHS/LHS" errors. - Nice error message for the illegal rewrite pattern "[X in t]" where "X" does not occur in "t". - "apply: n." doesn't (try to) clear "n" if "n" is a section variable. - Correctly handle (implicit) binders in have, suff and wlog tactics, like in "have f x : x \in [:: x]" where an extra binder is introduced for the type of "x". - "rewrite" progress check takes instantiated evars into account. - 'of' and '&' can be used in ssrbinders like in "have f of seq nat :...". - "move=> a b" now performs weak-head beta-reduction before introducing "b". - Interpret names after the "in" tactical with the right, Ltac-aware, function.