From 0c4a086210c6366c9ee1f091cc51ea5c92b5a903 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 19 Sep 2010 20:21:12 +0000
Subject: Fixing bug #2389 (keyword "Declare Instance" unknown from "coqdoc
 -g") but this lacks robustness since "coqdoc -g" will drop away any commands
 unknown from coqdoc, leading to possible synchronisation problems.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13440 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tools/coqdoc/cpretty.mll | 1 +
 1 file changed, 1 insertion(+)

(limited to 'tools')

diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 7ff4af7144..c018e66e34 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -324,6 +324,7 @@ let def_token =
   | "CoInductive"
   | "Equations"
   | "Instance"
+  | "Declare" space+ "Instance"
   | "Global" space+ "Instance"
 
 let decl_token =
-- 
cgit v1.2.3