Commit d36130f9 authored by Xavier Leroy's avatar Xavier Leroy
Browse files

Update the output of clightgen to pick the `$` notation from its new place

Follow-up to bb5dab84
parent 1a52f581
...@@ -455,8 +455,10 @@ let print_composite_definition p (Composite(id, su, m, a)) = ...@@ -455,8 +455,10 @@ let print_composite_definition p (Composite(id, su, m, a)) =
let prologue = "\ let prologue = "\
From Coq Require Import String List ZArith.\n\ From Coq Require Import String List ZArith.\n\
From compcert Require Import Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs.\n\ From compcert Require Import Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs.\n\
Import Clightdefs.ClightNotations.\n\
Local Open Scope Z_scope.\n\ Local Open Scope Z_scope.\n\
Local Open Scope string_scope.\n" Local Open Scope string_scope.\n\
Local Open Scope clight_scope.\n"
(* Naming the compiler-generated temporaries occurring in the program *) (* Naming the compiler-generated temporaries occurring in the program *)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment