Credits: addendum for version 6.3
The main changes in version V6.3 was the introduction of a few new tactics
and the extension of the guard condition for fixpoint definitions.
B. Barras extended the unification algorithm to complete partial terms
and solved various tricky bugs related to universes.
D. Delahaye developed the AutoRewrite tactic. He also designed the new
behavior of Intro and provided the tacticals First and
Solve.
J.-C. Filliâtre developed the Correctness tactic.
E. Giménez extended the guard condition in fixpoints.
H. Herbelin designed the new syntax for definitions and extended the
Induction tactic.
P. Loiseleur developed the Quote tactic and
the new design of the Auto
tactic, he also introduced the index of
errors in the documentation.
C. Paulin wrote the Focus command and introduced
the reduction functions in definitions, this last feature
was proposed by J.-F. Monin from CNET Lannion.
Orsay, Dec. 1999
Christine Paulin