From 6c4c3c7b2d144a15ca769e2722ec80b0480edf0b Mon Sep 17 00:00:00 2001
From: notin
Date: Mon, 17 Dec 2007 14:28:00 +0000
Subject: 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
---
 tools/coqdoc/pretty.mll | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'tools')

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" 
 
-- 
cgit v1.2.3