diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-02-06 14:04:29 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-02-06 14:04:29 +0100 |
| commit | a03dda71ff004c7a2b02654d96887609ef11d9fa (patch) | |
| tree | 65942e706688ef1ba5fc2b652bd756fa7ec4b78f /debug | |
| parent | 53c7c86c54fc8ec9d04afcc209d775b61922f627 (diff) | |
| download | compcert-kvx-a03dda71ff004c7a2b02654d96887609ef11d9fa.tar.gz compcert-kvx-a03dda71ff004c7a2b02654d96887609ef11d9fa.zip | |
Remove open AST.
The two types needed from AST are prefixed directly.
Diffstat (limited to 'debug')
| -rw-r--r-- | debug/DebugInformation.mli | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/debug/DebugInformation.mli b/debug/DebugInformation.mli index 66c4cd11..a5d1f806 100644 --- a/debug/DebugInformation.mli +++ b/debug/DebugInformation.mli @@ -10,9 +10,8 @@ (* *) (* *********************************************************************) -open AST open BinNums -open !C +open C open Camlcoq open DebugTypes open Sections @@ -79,11 +78,11 @@ val open_scope: atom -> int -> positive -> unit val close_scope: atom -> int -> positive -> unit -val start_live_range: (atom * atom) -> positive -> (int * int builtin_arg) -> unit +val start_live_range: (atom * atom) -> positive -> (int * int AST.builtin_arg) -> unit val end_live_range: (atom * atom) -> positive -> unit -val stack_variable: (atom * atom) -> int * int builtin_arg -> unit +val stack_variable: (atom * atom) -> int * int AST.builtin_arg -> unit val add_label: atom -> positive -> int -> unit |