diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-26 14:46:43 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-26 14:46:43 +0000 |
| commit | a29edb0a5e9d420a3780a7034aad4ef9cfe7c148 (patch) | |
| tree | 9b2ec00ba7d5a91491645c41cc41ab4f2bd07f1a /toplevel/protectedtoplevel.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 'toplevel/protectedtoplevel.ml')
| -rw-r--r-- | toplevel/protectedtoplevel.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/protectedtoplevel.ml b/toplevel/protectedtoplevel.ml index ad1beb553..7abb68eea 100644 --- a/toplevel/protectedtoplevel.ml +++ b/toplevel/protectedtoplevel.ml @@ -132,7 +132,7 @@ let rec parse_one_command_group input_channel = | Some(rank, e) -> (match e with | DuringCommandInterp(a,e1) - | Stdpp.Exc_located (a,DuringSyntaxChecking e1) -> + | DuringSyntaxChecking(a,e1) -> output_results_nl (acknowledge_command !global_request_id rank (Some e1)) @@ -167,7 +167,7 @@ let protected_loop input_chan = | DuringCommandInterp(loc, Vernacexpr.Quit) -> raise Vernacexpr.Quit | DuringCommandInterp(loc, Vernacexpr.Drop) -> raise Vernacexpr.Drop | DuringCommandInterp(loc, e) - | Stdpp.Exc_located (loc,DuringSyntaxChecking e) -> + | DuringSyntaxChecking(loc, e) -> explain_and_restart e | e -> explain_and_restart e in begin |