diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-26 16:41:36 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-26 16:41:36 +0000 |
commit | e31e4f88b20d7c32030ef6c0fe711f5fb7de2f66 (patch) | |
tree | 1c1740dbaf66646a3f044961b573c885b339b8bc /tools | |
parent | 5f1224c39d1c249b4cb0ce749ab91c3a9a4781c6 (diff) |
MAJ mot-cles
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5578 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
-rw-r--r-- | tools/coqdoc/pretty.mll | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index 935b3500b..02a0a7848 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -67,7 +67,7 @@ let is_proof = let t = Hashtbl.create 13 in List.iter (fun s -> Hashtbl.add t s true) - [ "Theorem"; "Lemma"; "Fact"; "Remark"; "Goal"; "Local"; + [ "Theorem"; "Lemma"; "Fact"; "Remark"; "Goal"; "Let"; "Correctness"; "Definition"; "Morphism" ]; fun s -> try Hashtbl.find t s with Not_found -> false @@ -236,19 +236,17 @@ let end_verb = "(*" space* "end" space+ "verb" space* "*)" *) let coq_command_to_hide = - "Implicit" 's'? space | - ("Recursive" space+)? "Tactic" space+ "Definition" space | + "Implicit" space | + "Ltac" space | "Require" space | "Load" space | - "Hint" 's'? space | + "Hint" space | "Transparent" space | "Opaque" space | - "Syntax" space | - "Grammar" space | ("Declare" space+ ("Morphism" | "Step") space) | "Section" space | "Variable" 's'? space | - "Hypothesis" space | + ("Hypothesis" | "Hypotheses") space | "End" space | ("Set" | "Unset") space+ "Printing" space+ "Coercions" space | "Declare" space+ ("Left" | "Right") space+ "Step" space @@ -487,7 +485,8 @@ and comment = parse and skip_proof = parse | "(*" { ignore (comment lexbuf); skip_proof lexbuf } - | "Save" | "Qed" | "Defined" | "Abort" | "Proof" { skip_to_dot lexbuf } + | "Save" | "Qed" | "Defined" + | "Abort" | "Proof" | "Admitted" { skip_to_dot lexbuf } | "Proof" space* '.' { skip_proof lexbuf } | identifier { skip_proof lexbuf } (* to avoid keywords within idents *) | eof { () } @@ -549,7 +548,7 @@ and printing_token = parse | Vernac_file (f,m) -> set_module m; let hf = m ^ ".html" in - set_out_file hf; + set_out_file hf; header (); coq_file f m; trailer (); |