aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/Program.tex
AgeCommit message (Collapse)Author
2007-01-31Fix typo.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9565 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-31Fix order of wf and measure arguments, patch Program doc.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9561 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-02Add doc on obligation solving commands.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9332 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-01Update Program/subtac documentation.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8890 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-07- Documentation of the Program tactics.msozeau
- 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 03:10:46 +0000