diff options
| -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 bc113cb838..cac0b0f769 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 61e2238754..c4b6c34b2a 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 1afd45b1f4..1ad7dcd0ad 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 |