From c072e4c5d9c48513d92d0ed0326e5fbf6991a645 Mon Sep 17 00:00:00 2001
From: Andrei Paskevich <andrei@lri.fr>
Date: Tue, 8 Mar 2016 17:09:23 +0100
Subject: [PATCH] Mlw: do not include Bool in HighOrd

also, we believe that VCgen does not introduce new dependencies
on built-in theories, so no need to reapply add_use.
---
 src/core/theory.ml |  3 +--
 src/mlw/pdecl.ml   |  2 +-
 src/mlw/pmodule.ml | 13 +++++--------
 3 files changed, 7 insertions(+), 11 deletions(-)

diff --git a/src/core/theory.ml b/src/core/theory.ml
index ee876e5c1..36c69cace 100644
--- a/src/core/theory.ml
+++ b/src/core/theory.ml
@@ -822,7 +822,6 @@ let bool_theory =
 
 let highord_theory =
   let uc = empty_theory (id_fresh "HighOrd") ["why3";"HighOrd"] in
-  let uc = use_export uc bool_theory in
   let uc = add_ty_decl uc ts_func in
   let uc = add_param_decl uc fs_func_app in
   close_theory uc
@@ -880,7 +879,7 @@ let () = Exn_printer.register
   | ClashSymbol s ->
       Format.fprintf fmt "Symbol %s is already defined in the current scope" s
   | UnknownMeta s ->
-      Format.fprintf fmt "Unknown metaproperty %s" s
+      Format.fprintf fmt "Unknown meta-property %s" s
   | KnownMeta m ->
       Format.fprintf fmt "Metaproperty %s is already registered with \
         a conflicting signature" m.meta_name
diff --git a/src/mlw/pdecl.ml b/src/mlw/pdecl.ml
index a9cc54ed6..acf83b7c6 100644
--- a/src/mlw/pdecl.ml
+++ b/src/mlw/pdecl.ml
@@ -480,7 +480,7 @@ let pd_int, pd_real, pd_equ = match builtin_theory.th_decls with
   | _ -> assert false
 
 let pd_func, pd_func_app = match highord_theory.th_decls with
-  | [{td_node = Use _bo}; {td_node = Decl df}; {td_node = Decl da}] ->
+  | [{td_node = Decl df}; {td_node = Decl da}] ->
       mk_decl (PDtype [mk_itd its_func [] [] []]) [df],
       mk_decl (PDlet ld_func_app) [da]
   | _ -> assert false
diff --git a/src/mlw/pmodule.ml b/src/mlw/pmodule.ml
index 94698e3d1..47b277aaf 100644
--- a/src/mlw/pmodule.ml
+++ b/src/mlw/pmodule.ml
@@ -298,7 +298,6 @@ let bool_module =
 
 let highord_module =
   let uc = empty_module dummy_env (id_fresh "HighOrd") ["why3";"HighOrd"] in
-  let uc = use_export uc bool_module in
   let uc = add_pdecl_no_logic uc pd_func in
   let uc = add_pdecl_no_logic uc pd_func_app in
   let m = close_module uc in
@@ -334,13 +333,11 @@ let add_use uc d = Sid.fold (fun id uc ->
 let add_pdecl ~vc uc d =
   let uc = add_use uc d in
   let dl = if vc then Vc.vc uc.muc_env uc.muc_known d else [] in
-  (* verification conditions might contain built-in symbols which
-     do not occur in the original declaration, so we call add_use.
-     However, we expect int.Int or any other library theory to
-     be in the context: importing them automatically seems to be
-     too invasive for the namespace. *)
-  let uc = List.fold_left (fun uc d -> add_pdecl (add_use uc d) d) uc dl in
-  add_pdecl uc d
+  (* verification conditions must not add additional dependencies
+     on built-in theories like TupleN or HighOrd. Also, we expect
+     int.Int or any other library theory to be in the context:
+     importing them automatically seems to be too invasive. *)
+  add_pdecl (List.fold_left add_pdecl uc dl) d
 
 (** {2 Cloning} *)
 
-- 
GitLab