diff options
| author | herbelin | 2009-10-26 14:46:43 +0000 |
|---|---|---|
| committer | herbelin | 2009-10-26 14:46:43 +0000 |
| commit | a29edb0a5e9d420a3780a7034aad4ef9cfe7c148 (patch) | |
| tree | 9b2ec00ba7d5a91491645c41cc41ab4f2bd07f1a /plugins/interface/coqparser.ml | |
| parent | 5dcc913519b8822ddf59eb3a356028f45f42cc3b (diff) | |
New cleaning phase of the Local/Global option management
- Clarification and documentation of the different styles of
Local/Global modifiers in vernacexpr.ml
- Addition of Global in sections for Open/Close Scope.
- Addition of Local for Ltac when not in sections.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12418 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/interface/coqparser.ml')
0 files changed, 0 insertions, 0 deletions