Release 2.0.5

Changes in 2.0.5 from 2.0.4

Additions

• Added support for (first-order) polymorphic definitions. Definitions
  such as the following are now accepted.

    Define fresh : A -> B -> prop by
      nabla x, fresh x M.
  

  In every use of the definition, the type arguments are implicitly
  instantiated. The type-checking for such definitions is identical to
  taking all the unbound variable names and quantifying them on the outside.
  In other words, for the above definition, the behavior of type-checking is
  the same as if there were:

    Kind A,B  type
    Define fresh : A -> B -> prop by
      nabla x, fresh x M.
  

  Once such a definition is type-checked, the defined symbols are added to
  the signature as new polymorphic constants, in a vein similar to the pi
  constant. Whenever it is used, the type arguments are implicitly
  instantiated based on the types of the arguments.

• Added support for (first-order) polymorphic theorems. A theorem such as
  the following is now accepted.

    Theorem prune[A] : forall E L, nabla (x:A), member (E x) L ->
       exists F, E = x\ F.
  

  The A here is a type parameter, which must be distinct from the other
  basic types in scope. To use such a theorem, you must supply enough
  arguments. An example:

    Theorem bar : forall E G, nabla (x:tm) (y:ty),
       member (E x y) G -> exists F, E = x\ y\ F.
    intros.
    apply prune[tm] to H1.
    apply prune[ty] to H1.
    search.
  

Tweaks to existing functionality

• The syntax for quantifiers now allows for multiple bound variables of the
  same type. Example:

    /* Type p i -> i -> prop. */
    forall (x y : i) (f g : i -> i), p (f (g y)) (g (f x))
  

• The apply tactic now takes an optional numerical argument that defines
  the search depth for automatic searches performed for omitted arguments. A
  bound of 0 means that no searches are attempted.

• The abbrev and unabbrev tactics now both take a list of hypotheses to
  (un)abbreviate. The display of abbreviations has also been compressed.

• Error messages in interactive mode are printed to stderr in addition to any
  other output file specified with -o.

• The monotone tactic now accepts hypothesis naming hints. (#91)

Bugfixes

• Query was broken since 2.0.4-beta2.
  (#69; reported by Ahn Ki Yung)
• Backchain now correctly takes into account inductive restrictions
  (#70; reported by Ahn Ki Yung)
• Search now correctly raises eigenvariables over support
  (#71; reported by Morten Rhiger)
• Undo/ProofGeneral now handles abbrev and unabbrev correctly.
• Do not normalize object sequents except when they occur shallowly
  among the assumptions or goal. Deep normalization is unsound.
  (Reported by Dale Miller)
• The apply tactic was invalidly raising guessed instances over
  nominal constants that already occur in the body of the lemma.
  (#96; reported by Ahn Ki Yung and Alwen Tiu)