diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml index 570067c07b196e5e0b7479f4891365a7a097d30a..6f6d3e93bda91b91387323ca0244041e263ab6de 100644 --- a/src/plugins/wp/Why3Import.ml +++ b/src/plugins/wp/Why3Import.ml @@ -33,6 +33,13 @@ let create_why3_env = W.Env.create_env (WConf.loadpath (WConf.get_main (WConf.read_config None))) end +let rec get_ty_symbols_from_ty (tys : W.Ty.tysymbol) (tymap) = + try W.Wstdlib.Mstr.find tymap tys + with Not_found -> + let ty = tys.tysymbol in + tymap <- Mty.add tys.tysymbol tymap; + + let () = Boot.Main.extend begin fun () ->