diff options
| author | notin | 2007-12-17 14:28:00 +0000 |
|---|---|---|
| committer | notin | 2007-12-17 14:28:00 +0000 |
| commit | 6c4c3c7b2d144a15ca769e2722ec80b0480edf0b (patch) | |
| tree | 3d2086ddc7d1262d15a79f34831cd3e5367fb721 | |
| parent | ec0eb7820be8ea48ed20d0e9dea88ce6f0693fa7 (diff) | |
Correction d'un bug dans Coqdoc: les mots clés liés aux sections étaient supprimés par l'option -g
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10386 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tools/coqdoc/pretty.mll | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index 6d088a70a7..8c46150a26 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -240,6 +240,10 @@ let gallina_ext = | "Infix" | "Tactic" space+ "Notation" | "Reserved" space+ "Notation" + | "Section" + | "Variable" 's'? + | ("Hypothesis" | "Hypotheses") + | "End" let commands = "Pwd" @@ -287,11 +291,7 @@ let gallina_kw_to_hide = | "Transparent" | "Opaque" | ("Declare" space+ ("Morphism" | "Step") ) - | "Section" | "Chapter" - | "Variable" 's'? - | ("Hypothesis" | "Hypotheses") - | "End" | ("Set" | "Unset") space+ "Printing" space+ "Coercions" | "Declare" space+ ("Left" | "Right") space+ "Step" |