aboutsummaryrefslogtreecommitdiffstats
path: root/debug/DebugTypes.mli
diff options
context:
space:
mode:
authorJacques-Henri Jourdan <jacques-henri.jourdan@inria.fr>2015-11-04 03:04:21 +0100
committerJacques-Henri Jourdan <jacques-henri.jourdan@inria.fr>2015-11-04 03:04:21 +0100
commit5664fddcab15ef4482d583673c75e07bd1e96d0a (patch)
tree878b22860e69405ba5cf6fd2798731dac8ce660c /debug/DebugTypes.mli
parentb960c83725d7e185ac5c6e3c0d6043c7dcd2f556 (diff)
parentfe73ed58ef80da7c53c124302a608948fb190229 (diff)
downloadcompcert-5664fddcab15ef4482d583673c75e07bd1e96d0a.tar.gz
compcert-5664fddcab15ef4482d583673c75e07bd1e96d0a.zip
Merge remote-tracking branch 'origin/master' into parser_fix
Diffstat (limited to 'debug/DebugTypes.mli')
-rw-r--r--debug/DebugTypes.mli6
1 files changed, 3 insertions, 3 deletions
diff --git a/debug/DebugTypes.mli b/debug/DebugTypes.mli
index 6a4f619c..b2f19f7a 100644
--- a/debug/DebugTypes.mli
+++ b/debug/DebugTypes.mli
@@ -68,7 +68,7 @@ type enum_type = {
enum_name: string;
enum_byte_size: int option;
enum_file_loc: location option;
- enum_enumerators: enumerator list;
+ enum_enumerators: enumerator list;
}
type int_type = {
@@ -115,7 +115,7 @@ type global_variable_information = {
gvar_type: int;
}
-type parameter_information =
+type parameter_information =
{
parameter_name: string;
parameter_ident: int;
@@ -150,7 +150,7 @@ type local_variable_information = {
lvar_static: bool; (* Static variable are mapped to symbols *)
}
-type scope_information =
+type scope_information =
{
scope_variables: int list; (* Variable and Scope ids *)
}