diff options
| author | msozeau | 2008-10-03 14:41:08 +0000 |
|---|---|---|
| committer | msozeau | 2008-10-03 14:41:08 +0000 |
| commit | 6832c60f741e6bfb2a850d567fd6a1dff7059393 (patch) | |
| tree | a31e0d9937437aa884c611a8554b80baaeae0811 /ide | |
| parent | b467ab92ef5bd124ae2bd19deea58765bd034f83 (diff) | |
Minor fixes related to coqdoc and --interpolate and the dependent
induction test-suite script.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11426 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index c4b6c34b2a..2c8d7b8db1 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -273,6 +273,7 @@ let rec attribute_of_vernac_command = function (* Commands *) | VernacDeclareTacticDefinition _ -> [] + | VernacCreateHintDb _ -> [] | VernacHints _ -> [] | VernacSyntacticDefinition _ -> [] | VernacDeclareImplicits _ -> [] |