aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/coqdoc/output.ml2
-rw-r--r--tools/coqdoc/pretty.mll2
2 files changed, 3 insertions, 1 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 067af63f2b..0522bbac08 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -42,7 +42,7 @@ let is_keyword =
"Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed";
"Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
"Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem";
- "Set"; "Unset"; "Variable"; "Variables";
+ "Set"; "Unset"; "Variable"; "Variables"; "Context";
"Notation"; "Reserved Notation"; "Tactic Notation";
"Delimit"; "Bind"; "Open"; "Scope";
"Boxed"; "Unboxed"; "Inline";
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index 36ed0472b2..d78aabbf93 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -1,3 +1,4 @@
+(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -246,6 +247,7 @@ let gallina_ext =
| "Tactic" space+ "Notation"
| "Reserved" space+ "Notation"
| "Section"
+ | "Context"
| "Variable" 's'?
| ("Hypothesis" | "Hypotheses")
| "End"