aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqwc.mll
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-05-31 15:05:23 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-05-31 15:05:23 +0000
commit45cf41f046a894165ce9782fbae37c4311c98d57 (patch)
treeab6d167405dcfa3b2849f6ab8a0ec4ea99be9463 /tools/coqwc.mll
parentfd9a6eb3375d586b53c8a3d44549261e188af6e0 (diff)
coqwc: Admitted
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7095 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqwc.mll')
-rw-r--r--tools/coqwc.mll2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqwc.mll b/tools/coqwc.mll
index 577645546..35004f79d 100644
--- a/tools/coqwc.mll
+++ b/tools/coqwc.mll
@@ -99,7 +99,7 @@ let dot = '.' (' ' | '\t' | '\n' | '\r' | eof)
let proof_start =
"Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness"
let proof_end =
- ("Save" | "Qed" | "Defined" | "Abort") [^'.']* '.'
+ ("Save" | "Qed" | "Defined" | "Abort" | "Admitted") [^'.']* '.'
(*s [spec] scans the specification. *)