aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-04-20 12:03:45 +0000
committerGravatar coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-04-20 12:03:45 +0000
commit38d5db3b7502c5a3e18290938422a7bc58aacc5a (patch)
tree541223a0385178784a047032a3d86f0d2ee476f2
parentbf439ba61e4a0df29b723505a49f488da777d6bc (diff)
Hints.... added next to Hint....
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1646 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--tools/gallina_lexer.mll1
1 files changed, 1 insertions, 0 deletions
diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll
index e3a81912a..98c838ed7 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 }