diff options
| author | msozeau | 2008-02-03 00:42:23 +0000 |
|---|---|---|
| committer | msozeau | 2008-02-03 00:42:23 +0000 |
| commit | 36fa70885150234159b0a6d8a1deb2d9fb3d2b8a (patch) | |
| tree | a16ec5f253ee4fbc529c59e22abab2a46d8c28ab /doc/refman | |
| parent | c3f187d2eee5a99bf1a903059a3f18ff77560c98 (diff) | |
Add new files theories/Program/Basics.v and theories/Classes/Relations.v
for basic functional programming and relation
definitions respectively.
Classes.Relations also includes the definition of Morphism
and instances for the standard morphisms and relations (eq, iff, impl,
inverse and complement). The class_setoid.ml4 [setoid_rewrite] tactic
has been reimplemented on top of these definitions, hence it doesn't
require a setoid implementation anymore. It also generates obligations
for missing reflexivity proofs, like the current setoid_rewrite. It has
not been tested on large examples but it should handle directions and
occurences. Works with in if no obligations are generated at this time.
What's missing is being able to rewrite by a lemma instead of a simple
hypothesis with no premises.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10502 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 4a2dad8cab..a58125dc09 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1608,7 +1608,7 @@ defined in the same file: \begin{Variants} \item {\tt dependent induction {\ident} generalizing {\ident$_1$} \dots - {\ident$_n$}}\tacindex{dependent induction ... generalizing} + {\ident$_n$}}\tacindex{dependent induction \dots\ generalizing} Does dependent induction on the hypothesis {\ident} but first generalizes the goal by the given variables so that they are @@ -1616,9 +1616,9 @@ defined in the same file: to do with the variables that are inside some constructors in the induction hypothesis. The other ones need not be further generalized. -\item {\tt dependent destruction}\tacindex{dependent destruction} +\item {\tt dependent destruction {\ident}}\tacindex{dependent destruction} - Does the generalization of the instance but uses {\tt destruct} + Does the generalization of the instance {\ident} but uses {\tt destruct} instead of {\tt induction} on the generalized hypothesis. This gives results equivalent to {\tt inversion} or {\tt dependent inversion} if the hypothesis is dependent. |