aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc/cpretty.mll
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-12-26 17:07:20 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-12-26 17:07:20 +0000
commit34416087ebfa54a7ed780bf756fa99a2a3d0f180 (patch)
tree65e1f5c3b3fda2929e1f41bc566d24336b14b4ac /tools/coqdoc/cpretty.mll
parent1543d091ad7923cab049da8871ec010ab8a6d125 (diff)
Coqdoc: Fixing missing newline when using "Proof term."
(bug apparently introduced by r11880). Fixing also a "body_bol" which apparently should be a "bol". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14866 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc/cpretty.mll')
-rw-r--r--tools/coqdoc/cpretty.mll12
1 files changed, 9 insertions, 3 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 89047e83c..43a4b0eb9 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -306,7 +306,12 @@ let thm_token =
let prf_token =
"Next" space+ "Obligation"
- | "Proof" (space* "." | space+ "with")
+ | "Proof" (space* "." | space+ "with" | space+ "using")
+
+let immediate_prf_token =
+ (* Approximation of a proof term, if not in the prf_token case *)
+ (* To be checked after prf_token *)
+ "Proof" space* [^ '.' 'w' 'u']
let def_token =
"Definition"
@@ -382,7 +387,8 @@ let commands =
| ("Hypothesis" | "Hypotheses")
| "End"
-let end_kw = "Qed" | "Defined" | "Save" | "Admitted" | "Abort"
+let end_kw =
+ immediate_prf_token | "Qed" | "Defined" | "Save" | "Admitted" | "Abort"
let extraction =
"Extraction"
@@ -605,7 +611,7 @@ and coq = parse
| prf_token
{ let eol =
if not !Cdglobals.gallina then
- begin backtrack lexbuf; body_bol lexbuf end
+ begin backtrack lexbuf; body lexbuf end
else
let s = lexeme lexbuf in
let eol =