Commit cde5c55a authored by Andrei Paskevich's avatar Andrei Paskevich

fix #15063

parent ac1f7b76
......@@ -457,8 +457,11 @@ let read_config_rc conf_file =
exception ConfigFailure of string (* filename *) * string
let get_dirname filename =
Filename.dirname (absolute_filename (Sys.getcwd ()) filename)
let get_config (filename,rc) =
let dirname = Filename.dirname filename in
let dirname = get_dirname filename in
let rc, main =
match get_section rc "main" with
| None -> raise (ConfigFailure (filename, "no main section"))
......@@ -572,7 +575,7 @@ let filter_one_prover whyconf fp =
(** merge config *)
let merge_config config filename =
let dirname = Filename.dirname filename in
let dirname = get_dirname filename in
let rc = Rc.from_file filename in
(** modify main *)
let main = match get_section rc "main" with
......
......@@ -1643,7 +1643,7 @@ let scroll_to_loc ?(yalign=0.0) ~color loc =
if f <> !current_file then
begin
let lang =
if Filename.check_suffix f ".why" ||
if Filename.check_suffix f ".why" ||
Filename.check_suffix f ".mlw"
then why_lang else any_lang f
in
......
......@@ -770,10 +770,6 @@ let lambda_invariant lenv pvs eff lam =
(* specification handling *)
let rec dty_of_ty ty = match ty.ty_node with
| Ty.Tyapp (ts, tyl) -> Denv.tyapp ts (List.map dty_of_ty tyl)
| Ty.Tyvar v -> Denv.tyuvar v
let create_variant lenv (t,r) =
let t = Typing.type_term lenv.th_at (find_vs lenv.mod_uc lenv.log_vars) t in
count_term_tuples t;
......
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