diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/jib/anf.ml | 2 | ||||
| -rw-r--r-- | src/jib/jib_compile.ml | 3 |
2 files changed, 3 insertions, 2 deletions
diff --git a/src/jib/anf.ml b/src/jib/anf.ml index 5165904d..dbbb10e0 100644 --- a/src/jib/anf.ml +++ b/src/jib/anf.ml @@ -670,7 +670,7 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = let aexp2 = anf exp2 in let aval1, wrap1 = to_aval aexp1 in let aval2, wrap2 = to_aval aexp2 in - wrap1 (wrap2 (mk_aexp (AE_app (mk_id "cons", [aval1; aval2], unit_typ)))) + wrap1 (wrap2 (mk_aexp (AE_app (mk_id "sail_cons", [aval1; aval2], unit_typ)))) | E_id id -> let lvar = Env.lookup_id id (env_of exp) in diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml index 7e062c5a..2066021e 100644 --- a/src/jib/jib_compile.ml +++ b/src/jib/jib_compile.ml @@ -1568,8 +1568,9 @@ let sort_ctype_defs cdefs = let compile_ast ctx (Defs defs) = let assert_vs = Initial_check.extern_of_string (mk_id "sail_assert") "(bool, string) -> unit" in let exit_vs = Initial_check.extern_of_string (mk_id "sail_exit") "unit -> unit" in + let cons_vs = Initial_check.extern_of_string (mk_id "sail_cons") "forall ('a : Type). ('a, list('a)) -> list('a)" in - let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs])) } in + let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs; cons_vs])) } in if !opt_memo_cache then (try |