diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-15 18:59:07 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-15 18:59:07 +0000 |
| commit | 566e21af6792406715e79df5c61a3cc715b15c66 (patch) | |
| tree | 5bd0a8c88f110e6fbfe2b2d25778fd3a01e0a833 /parsing/g_vernac.ml4 | |
| parent | 77ba6079eef1099a34bfcff01fe36298392e3fdf (diff) | |
Document Generalizable Variables, and change syntax to
[Generalizable (All|No) Variables (ident+)?], also update
type classes documentation to reflect the latest changes
in instance decls. Fix a bug in [Util.list_split_when].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12525 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index a0ee06683..3bc27965a 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -553,9 +553,11 @@ GEXTEND Gram | IDENT "Implicit"; ["Type" | IDENT "Types"]; idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c) - | IDENT "Generalizable"; ["Variable" | IDENT "Variables"]; - gen = [ IDENT "none" -> None | IDENT "all" -> Some [] | - idl = LIST1 identref -> Some idl ] -> + | IDENT "Generalizable"; + gen = [IDENT "All"; IDENT "Variables" -> Some [] + | IDENT "No"; IDENT "Variables" -> None + | [IDENT "Variable" | IDENT "Variables"]; + idl = LIST1 identref -> Some idl ] -> VernacGeneralizable (use_non_locality (), gen) ] ] ; implicit_name: |