coq/contrib/subtac/FunctionalExtensionality.v, branch master

Move Program tactics into a proper theories/ directory as they are general purpose and can be used directly be the user. Document them. Change Prelude to disambiguate an import of a Tactics module.

2007-08-07T18:36:25+00:00

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

Add a parameter to QuestionMark evar kind to say it can be turned into an obligations (even an opaque one).

2007-03-19T16:54:25+00:00

Change cast_type to include the converted-to type or nothing in case of a Coerce cast, required much minor changes.
Various little subtac changes.


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

The right tactics for definitions using measures.

2007-02-28T09:16:44+00:00

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

Various subtac fixes.

2007-01-15T10:06:40+00:00

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

Subtac fixes, support for reasoning on wf defs.

2007-01-08T17:44:28+00:00

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