diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-18 16:10:45 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-18 16:10:45 +0000 |
| commit | e2b35440ac709a3702ff30ab74c4a324e75929b2 (patch) | |
| tree | 57136c5ee9abcfdc3183da05ba4f9a0a8e8bf140 | |
| parent | d6f4f3f3dc92d805bc046bcdbc30dd7df65fb4aa (diff) | |
- Rebranchement backtrack du langage déclaratif dans Coqide
- Divers: message d'erreur et typo relatifs au langage déclaratif
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11237 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | doc/refman/RefMan-decl.tex | 4 | ||||
| -rw-r--r-- | ide/coq.ml | 6 | ||||
| -rw-r--r-- | proofs/refiner.ml | 4 |
3 files changed, 6 insertions, 8 deletions
diff --git a/doc/refman/RefMan-decl.tex b/doc/refman/RefMan-decl.tex index bc113cb83..cac0b0f76 100644 --- a/doc/refman/RefMan-decl.tex +++ b/doc/refman/RefMan-decl.tex @@ -101,7 +101,7 @@ Here is a complete formal description of the syntax for DPL commands. {\tt per} ({\tt cases}$|${\tt induction}) {\tt on} \term \\ & $|$ & {\tt per cases of} type justification \\ & $|$ & {\tt suppose} \zeroone{\nelist{ident}{,} {\tt and}}~ - {\tt is is }pattern\\ + {\tt it is }pattern\\ & & \zeroone{{\tt such that} \nelist{statement} {\tt and} \zeroone{{\tt and} \{{\tt we have}\}-clause}} \\ & $|$ & {\tt end} ({\tt proof} $|$ {\tt claim} $|$ {\tt focus} $|$ {\tt cases} $|$ {\tt induction}) \\ @@ -276,7 +276,7 @@ let x be such that H:(x=2). Abort. \end{coq_eval} -In this example, you can also see the creation of a temporary name {\tt \_hyp}. +In this example, you can also see the creation of a temporary name {\tt \_fact}. \subsection{Iterated equalities} diff --git a/ide/coq.ml b/ide/coq.ml index 61e223875..c4b6c34b2 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -248,9 +248,9 @@ let rec attribute_of_vernac_command = function | VernacSolveExistential _ -> [SolveCommand] (* MMode *) - | VernacDeclProof -> [] - | VernacReturn -> [] - | VernacProofInstr _ -> [] + | VernacDeclProof -> [SolveCommand] + | VernacReturn -> [SolveCommand] + | VernacProofInstr _ -> [SolveCommand] (* Auxiliary file and library management *) | VernacRequireFrom _ -> [] diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 1afd45b1f..1ad7dcd0a 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -754,9 +754,7 @@ let extract_open_pftreestate pts = let extract_pftreestate pts = if pts.tstack <> [] then - errorlabstrm "extract_pftreestate" - (str"Cannot extract from a proof-tree in which we have descended;" ++ - spc () ++ str"Please ascend to the root"); + errorlabstrm "extract_pftreestate" (str"Proof blocks need to be closed"); let pfterm,subgoals = extract_open_pftreestate pts in let exl = Evarutil.non_instantiated pts.tpfsigma in if subgoals <> [] or exl <> [] then |