Merge branch 'sail2' into rmem_interpreter

1 files changed, 7 insertions, 2 deletions

diff --git a/src/c_backend.ml b/src/c_backend.ml
index 65702764..7cda4668 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -1399,9 +1399,11 @@ let compile_type_def ctx (TD_aux (type_def, _)) =
      CTD_struct (id, Bindings.bindings ctors),
      { ctx with records = Bindings.add id ctors ctx.records }
 
-  | TD_variant (id, _, _, tus, _) ->
+  | TD_variant (id, _, typq, tus, _) ->
      let compile_tu = function
-       | Tu_aux (Tu_ty_id (typ, id), _) -> ctyp_of_typ ctx typ, id
+       | Tu_aux (Tu_ty_id (typ, id), _) ->
+          let ctx = { ctx with local_env = add_typquant (id_loc id) typq ctx.local_env } in
+          ctyp_of_typ ctx typ, id
      in
      let ctus = List.fold_left (fun ctus (ctyp, id) -> Bindings.add id ctyp ctus) Bindings.empty (List.map compile_tu tus) in
      CTD_variant (id, Bindings.bindings ctus),
@@ -1761,6 +1763,9 @@ let rec compile_def ctx = function
   (* Only the parser and sail pretty printer care about this. *)
   | DEF_fixity _ -> [], ctx
 
+  (* We just ignore any pragmas we don't want to deal with. *)
+  | DEF_pragma _ -> [], ctx
+
   | DEF_internal_mutrec fundefs ->
      let defs = List.map (fun fdef -> DEF_fundef fdef) fundefs in
      List.fold_left (fun (cdefs, ctx) def -> let cdefs', ctx = compile_def ctx def in (cdefs @ cdefs', ctx)) ([], ctx) defs