From 2bdcd093b357adb2185518dabbafd1a0b9279044 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Tue, 27 Mar 2012 07:41:19 +0200
Subject: Imported Upstream version 8.3.pl4

---
 tools/coqdoc/cpretty.mll | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

(limited to 'tools/coqdoc')

diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 63850bd5..a2bcb987 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: cpretty.mll 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(*i $Id: cpretty.mll 14868 2011-12-26 17:07:24Z herbelin $ i*)
 
 (*s Utility functions for the scanners *)
 
@@ -309,7 +309,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"
@@ -384,7 +389,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"
@@ -607,7 +613,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 =
-- 
cgit v1.2.3