Rename span into raw_span

4 files changed, 20 insertions, 20 deletions

diff --git a/compiler/Errors.ml b/compiler/Errors.ml
index 30887593..d084df51 100644
--- a/compiler/Errors.ml
+++ b/compiler/Errors.ml
@@ -1,13 +1,13 @@
 let log = Logging.errors_log
 
 let meta_to_string (meta : Meta.meta) =
-  let span = meta.span in
-  let file = match span.file with Virtual s | Local s -> s in
+  let raw_span = meta.span in
+  let file = match raw_span.file with Virtual s | Local s -> s in
   let loc_to_string (l : Meta.loc) : string =
     string_of_int l.line ^ ":" ^ string_of_int l.col
   in
-  "Source: '" ^ file ^ "', lines " ^ loc_to_string span.beg_loc ^ "-"
-  ^ loc_to_string span.end_loc
+  "Source: '" ^ file ^ "', lines " ^ loc_to_string raw_span.beg_loc ^ "-"
+  ^ loc_to_string raw_span.end_loc
 
 let format_error_message (meta : Meta.meta option) (msg : string) =
   let meta =
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 8efb59fb..65f7b06e 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -1249,7 +1249,7 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx)
        Some def.llbc_name
      else None
    in
-   extract_comment_with_span ctx fmt
+   extract_comment_with_raw_span ctx fmt
      [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases clause" ]
      name def.meta.span);
   F.pp_print_space fmt ();
@@ -1316,7 +1316,7 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
-  extract_comment_with_span ctx fmt
+  extract_comment_with_raw_span ctx fmt
     [ "[" ^ name_to_string ctx def.llbc_name ^ "]: termination measure" ]
     None def.meta.span;
   F.pp_print_space fmt ();
@@ -1371,7 +1371,7 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
   let def_name = ctx_get_decreases_proof def.meta def.def_id def.loop_id ctx in
   (* syntax <def_name> term ... term : tactic *)
   F.pp_print_break fmt 0 0;
-  extract_comment_with_span ctx fmt
+  extract_comment_with_raw_span ctx fmt
     [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases_by tactic" ]
     None def.meta.span;
   F.pp_print_space fmt ();
@@ -1418,7 +1418,7 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter)
       Some def.llbc_name
     else None
   in
-  extract_comment_with_span ctx fmt comment name def.meta.span
+  extract_comment_with_raw_span ctx fmt comment name def.meta.span
 
 (** Extract a function declaration.
 
@@ -1892,7 +1892,7 @@ let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter)
       Some global.llbc_name
     else None
   in
-  extract_comment_with_span ctx fmt
+  extract_comment_with_raw_span ctx fmt
     [ "[" ^ name_to_string ctx global.llbc_name ^ "]" ]
     name global.meta.span;
   F.pp_print_space fmt ();
@@ -2354,7 +2354,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
        Some decl.llbc_name
      else None
    in
-   extract_comment_with_span ctx fmt
+   extract_comment_with_raw_span ctx fmt
      [ "Trait declaration: [" ^ name_to_string ctx decl.llbc_name ^ "]" ]
      name decl.meta.span);
   F.pp_print_break fmt 0 0;
@@ -2653,7 +2653,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
          Some (trait_decl.llbc_generics, decl_ref.decl_generics) )
      else (None, None)
    in
-   extract_comment_with_span ctx fmt
+   extract_comment_with_raw_span ctx fmt
      [ "Trait implementation: [" ^ name_to_string ctx impl.llbc_name ^ "]" ]
      (* TODO: why option option for the generics? Looks like a bug in OCaml!? *)
      name ?generics:(Some generics) impl.meta.span);
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 6a6067de..44744577 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -1146,17 +1146,17 @@ let extract_comment (fmt : F.formatter) (sl : string list) : unit =
   F.pp_print_string fmt rd;
   F.pp_close_box fmt ()
 
-let extract_comment_with_span (ctx : extraction_ctx) (fmt : F.formatter)
+let extract_comment_with_raw_span (ctx : extraction_ctx) (fmt : F.formatter)
     (sl : string list) (name : Types.name option)
     ?(generics : (Types.generic_params * Types.generic_args) option = None)
-    (span : Meta.span) : unit =
-  let file = match span.file with Virtual s | Local s -> s in
+    (raw_span : Meta.raw_span) : unit =
+  let file = match raw_span.file with Virtual s | Local s -> s in
   let loc_to_string (l : Meta.loc) : string =
     string_of_int l.line ^ ":" ^ string_of_int l.col
   in
-  let span =
-    "Source: '" ^ file ^ "', lines " ^ loc_to_string span.beg_loc ^ "-"
-    ^ loc_to_string span.end_loc
+  let raw_span =
+    "Source: '" ^ file ^ "', lines " ^ loc_to_string raw_span.beg_loc ^ "-"
+    ^ loc_to_string raw_span.end_loc
   in
   let name =
     match (name, generics) with
@@ -1169,7 +1169,7 @@ let extract_comment_with_span (ctx : extraction_ctx) (fmt : F.formatter)
           ^ name_with_generics_to_pattern_string ctx.trans_ctx name params args;
         ]
   in
-  extract_comment fmt (sl @ [ span ] @ name)
+  extract_comment fmt (sl @ [ raw_span ] @ name)
 
 let extract_trait_clause_type (meta : Meta.meta) (ctx : extraction_ctx)
     (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t)
@@ -1414,7 +1414,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
        Some def.llbc_name
      else None
    in
-   extract_comment_with_span ctx fmt
+   extract_comment_with_raw_span ctx fmt
      [ "[" ^ name_to_string ctx def.llbc_name ^ "]" ]
      name def.meta.span);
   F.pp_print_break fmt 0 0;
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 451767f8..a07167a8 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -50,7 +50,7 @@ type region_group_id = T.region_group_id [@@deriving show, ord]
 type mutability = Mut | Const [@@deriving show, ord]
 type loc = Meta.loc [@@deriving show, ord]
 type file_name = Meta.file_name [@@deriving show, ord]
-type span = Meta.span [@@deriving show, ord]
+type raw_span = Meta.raw_span [@@deriving show, ord]
 type meta = Meta.meta [@@deriving show, ord]
 
 (** The assumed types for the pure AST.