handles explicit function calls, names meta variables in patterns

(in V8 the name is not a number), explicitation of arguments with names
(but not with rank anymore), the refine tactic now has its own operator
the structure information for hypotheses in induction is now handled
as in intro, the tactic instantiate has been modified to use clauses,
the wildcard rule for Ltac pattern matching on goals has been added
and the possibility to refer to types of values and instantiated contexts
in values in Ltac have been added.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5232 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions