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.3pl1

Release Notes
While the .v files are unchanged, the plugin received the following fixes:

- Avoid defining new keywords when the ML plugin is loaded (or linked
  statically): all keywords are defined inside ssreflect.SsrSyntax.
  The plugin, even if loaded, turns off all incompatible features, like
  the extended rewrite syntax, is ssreflect.SsrSyntax is not imported.
  This allows for developing theories using SSR's syntax but does not
  impose to their users SSR's syntax (See section 2.2 Compatibility
  issues in the manual).

- Anomaly is no more raised by the Search command when a non existing
  constant is mentioned in the arguments

- Better error message for iterated commands (do, rewrite !).
    example: rewrite 2!H
    was:  Error: No occurrence of redex a
    is:   Error: At iteration 2: No occurrence of redex a

- The have and suffices tactics, when used with the 1.3 binders feature,
  correctly honour the "Automatic Introduction" flag

- New alias "Canonical" for "Canonical Structure"

Documentation has also been updated accordingly.