diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdoc/output.ml | 4 | ||||
| -rw-r--r-- | tools/coqdoc/pretty.mll | 12 |
2 files changed, 11 insertions, 5 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 1cbee60463..647cc5da3f 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -46,9 +46,11 @@ let is_keyword = "Delimit"; "Bind"; "Open"; "Scope"; "Boxed"; "Unboxed"; "Arguments"; + "Instance"; "Class"; "where"; "Instantiation"; (* Program *) "Program Definition"; "Program Fixpoint"; "Program Lemma"; "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next"; + "Program Instance"; (*i (* correctness *) "array"; "assert"; "begin"; "do"; "done"; "else"; "end"; "if"; "in"; "invariant"; "let"; "of"; "ref"; "state"; "then"; "variant"; @@ -366,7 +368,7 @@ module Html = struct module_ref m s | Ref (m,fullid) -> ident_ref m fullid s - | Mod _ | Ref _ -> + | Mod _ -> raw_ident s) with Not_found -> raw_ident s diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index 8c46150a26..2af5bda093 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -207,6 +207,7 @@ let thm_token = let def_token = "Definition" | "Let" + | "Class" | "SubClass" | "Example" | "Local" @@ -214,11 +215,10 @@ let def_token = | "CoFixpoint" | "Record" | "Structure" + | "Instance" | "Scheme" | "Inductive" | "CoInductive" - | "Program" space+ "Definition" - | "Program" space+ "Fixpoint" let decl_token = "Hypothesis" @@ -263,12 +263,17 @@ let commands = | "Check" | "Type" + | "Section" + | "Chapter" + | "Variable" 's'? + | ("Hypothesis" | "Hypotheses") + | "End" + let extraction = "Extraction" | "Recursive" space+ "Extraction" | "Extract" - let gallina_kw = thm_token | def_token | decl_token | gallina_ext | commands | extraction let prog_kw = @@ -291,7 +296,6 @@ let gallina_kw_to_hide = | "Transparent" | "Opaque" | ("Declare" space+ ("Morphism" | "Step") ) - | "Chapter" | ("Set" | "Unset") space+ "Printing" space+ "Coercions" | "Declare" space+ ("Left" | "Right") space+ "Step" |