From 625a129d5e9b200399a147111f191abe84282aa4 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 6 Nov 2009 03:01:57 +0000
Subject: Misc fixes. - Correct backtracking function of coqdoc to handle the
 _p fields of lexers - Try a better typesetting of [[ ]] inline code
 considering it as blocks and not purely inline code like [ ] escapings. -
 Rework latex macros for better factorization and support external references
 in pdf output. - Better criterion for generalization of variables in
 dependent elimination tactic and better error message in
 [specialize_hypothesis]. - In autounfold, don't put the core unfolds by
 default.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12474 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_vernac.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 2fd822636e..c21185c511 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -552,7 +552,7 @@ GEXTEND Gram
       | IDENT "Generalizable"; ["Variable" | IDENT "Variables"];
            gen = [ IDENT "none" -> None | IDENT "all" -> Some [] | 
 	       idl = LIST1 identref -> Some idl ] ->
-	     VernacGeneralizable (use_section_locality (), gen) ] ]
+	     VernacGeneralizable (use_non_locality (), gen) ] ]
   ;
   implicit_name:
     [ [ "!"; id = ident -> (id, false, true)
-- 
cgit v1.2.3