From 38d5db3b7502c5a3e18290938422a7bc58aacc5a Mon Sep 17 00:00:00 2001
From: coq
Date: Fri, 20 Apr 2001 12:03:45 +0000
Subject: Hints.... added next to Hint....

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

diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll
index e3a81912a8..98c838ed76 100644
--- a/tools/gallina_lexer.mll
+++ b/tools/gallina_lexer.mll
@@ -40,6 +40,7 @@ rule action = parse
   | "Definition" space  { print "Definition "; body_def lexbuf;
 			  cRcpt := 1; action lexbuf }
   | "Hint" space        { skip_until_point lexbuf ; action lexbuf }
+  | "Hints" space        { skip_until_point lexbuf ; action lexbuf }
   | "Transparent" space { skip_until_point lexbuf ; action lexbuf }
   | "Immediate"	space   { skip_until_point lexbuf ; action lexbuf }
   | "Syntax" space      { skip_until_point lexbuf ; action lexbuf }
-- 
cgit v1.2.3