diff options
| author | filliatr | 2003-12-16 15:54:06 +0000 |
|---|---|---|
| committer | filliatr | 2003-12-16 15:54:06 +0000 |
| commit | 22a24e1cadd4e1206db195c9ef19ca3130eb1bc8 (patch) | |
| tree | b679e3a64f57c8738388d08cc6627cc7a518f23a /doc/Tutorial.tex | |
| parent | d418004b79b5f95898eafa0b5376d5afc30cd699 (diff) | |
tactiques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8401 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/Tutorial.tex')
| -rwxr-xr-x | doc/Tutorial.tex | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/Tutorial.tex b/doc/Tutorial.tex index ef927764b2..93b5276f9a 100755 --- a/doc/Tutorial.tex +++ b/doc/Tutorial.tex @@ -315,7 +315,7 @@ Now $H'$ applies: apply H'. \end{coq_example} -And we may now conclude the proof as before, with \verb:Exact HA.: +And we may now conclude the proof as before, with \verb:exact HA.: Actually, we may not bother with the name \verb:HA:, and just state that the current goal is solvable from the current local assumptions: \begin{coq_example} @@ -331,7 +331,7 @@ Save trivial_lemma. \end{coq_example} As a comment, the system shows the proof script listing all tactic -commands used in the proof. % ligne blanche apres Exact HA?? +commands used in the proof. % ligne blanche apres exact HA?? Let us redo the same proof with a few variations. First of all we may name the initial goal as a conjectured lemma: @@ -535,7 +535,7 @@ It is not easy to understand the notation for proof terms without a few explanations. The square brackets, such as \verb+[H:A\/B]+, correspond to \verb:Intro H:, whereas a subterm such as \verb:(or_intror: \verb:B A H0): -corresponds to the sequence \verb:Apply or_intror; Exact H0:. The extra +corresponds to the sequence \verb:Apply or_intror; exact H0:. The extra arguments \verb:B: and \verb:A: correspond to instantiations to the generic combinator \verb:or_intror:, which are effected automatically by the tactic \verb:Apply: when pattern-matching a goal. The specialist will of course |