Home My Page Projects CoqFiniteGroups
Summary Activity Forums Tracker Lists Tasks Docs News SCM Files

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.


- 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
- "elim" correctly handles delta expansions and let-ins in the
  eliminator's type.
- "elim"'s predicate is typechecked to avoid generating an ill-typed
- 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
- Interpret names after the "in" tactical with the right, Ltac-aware,