diff options
| author | Enrico Tassi | 2014-12-19 12:00:44 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-12-19 12:00:57 +0100 |
| commit | ab7d96a1d7c1bd44cf3bca5f593b947975117ed8 (patch) | |
| tree | 346eac1f9ccddd701a6d160f493fd070bc84d09f /parsing | |
| parent | 96906c2a1ba9426271a4048bfa8b3991db51c192 (diff) | |
Better doc and a few fixes for Proof using.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 77ba41f4e0..ccfe3cc8c1 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -460,7 +460,7 @@ GEXTEND Gram | IDENT "End"; id = identref -> VernacEndSegment id (* Naming a set of section hyps *) - | IDENT "Package"; id = identref; ":="; expr = section_subset_descr -> + | IDENT "Collection"; id = identref; ":="; expr = section_subset_descr -> VernacNameSectionHypSet (id, expr) (* Requiring an already compiled module *) |