coq/contrib/subtac/FixSub.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

Documentation of Program and its tactics, fix enormous interaction bug due to bad cache handling.

2007-07-19T22:10:16+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10032 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

Coqdoc patch for Program, fix xlate.ml warning and little subtac fixes.

2007-01-29T12:20:10+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9550 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

Mutually structurally recursive defs and rec using measures added.

2006-06-22T08:51:24+00:00

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

Fixes for new unification, not used in default version as it really changes unification.

2006-04-10T16:33:52+00:00

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

- Documentation of the Program tactics.

2006-04-07T15:08:12+00:00

- Fixes to the subtac implementation, utility tactic to apply existentials to a function and build a dependent sum out of name, constr lists.
Also defined a Utils coq module for tactics related to subsets and the projections for ex in Prop.
- Enhancements to inference algorithm added but not used in the default version as there are some remaining bugs.



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

Made pretyping a functor over a coercion implementation. Pretyping.Default uses the original Coercion implementation.

2006-03-22T15:36:58+00:00

Updated contributions that called pretyping to use the default impl.
Also update subtac using the functor, do some renamings and add interfaces for all files.



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

Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.

2006-03-13T17:38:17+00:00

May cause make world to fail because of dependency problems, make depend clean
world should fix that (hopefully).


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