Commit 15e0350c authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Avoiding declaring ts_mark in two separate theories.

parent efcac6e1
......@@ -401,7 +401,7 @@ let mod_prelude env =
let pd_exit = create_exn_decl xs_exit in
let pd_old = create_val_decl (LetV Mlw_wp.pv_old) in
let uc = empty_module env (id_fresh "Prelude") ["why3"] in
let uc = add_decl uc (Decl.create_ty_decl Mlw_wp.ts_mark) in
let uc = use_export_theory uc Mlw_wp.mark_theory in
let uc = add_pdecl ~wp:false uc pd_old in
let uc = add_pdecl ~wp:false uc pd_exit in
close_module uc
......@@ -47,9 +47,14 @@ let fs_old =
let ty = ty_var (create_tvsymbol (id_fresh "a")) in
create_lsymbol (id_fresh "old") [ty] (Some ty)
let mark_theory =
let uc = create_theory ~path:["why3"] (id_fresh "Mark") in
let uc = add_ty_decl uc ts_mark in
close_theory uc
let th_mark_at =
let uc = create_theory (id_fresh "WP builtins: at") in
let uc = add_ty_decl uc ts_mark in
let uc = use_export uc mark_theory in
let uc = add_param_decl uc fs_at in
close_theory uc
......@@ -27,6 +27,7 @@ val fs_old : Term.lsymbol
val t_at_old : Term.term -> Term.term
val mark_theory : Theory.theory
val th_mark_at : Theory.theory
val th_mark_old : Theory.theory
Markdown is supported
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