Commit 947e68e1 authored by David Hauzar's avatar David Hauzar
Browse files

Removing counter-example option from whyconf.

parent 94debda2
...@@ -203,7 +203,6 @@ let loadpath m = ...@@ -203,7 +203,6 @@ let loadpath m =
let timelimit m = m.timelimit let timelimit m = m.timelimit
let memlimit m = m.memlimit let memlimit m = m.memlimit
let running_provers_max m = m.running_provers_max let running_provers_max m = m.running_provers_max
let cntexample m = m.cntexample
exception StepsCommandNotSpecified of string exception StepsCommandNotSpecified of string
...@@ -259,7 +258,6 @@ let empty_main = ...@@ -259,7 +258,6 @@ let empty_main =
memlimit = 1000; (* 1 Mb *) memlimit = 1000; (* 1 Mb *)
running_provers_max = 2; (* two provers run in parallel *) running_provers_max = 2; (* two provers run in parallel *)
plugins = []; plugins = [];
cntexample = true;
} }
let default_main = let default_main =
...@@ -278,7 +276,6 @@ let set_main rc main = ...@@ -278,7 +276,6 @@ let set_main rc main =
let section = let section =
set_int section "running_provers_max" main.running_provers_max in set_int section "running_provers_max" main.running_provers_max in
let section = set_stringl section "plugin" main.plugins in let section = set_stringl section "plugin" main.plugins in
let section = set_bool section "get-ce" main.cntexample in
set_section rc "main" section set_section rc "main" section
exception NonUniqueId exception NonUniqueId
...@@ -512,7 +509,6 @@ let load_main dirname section = ...@@ -512,7 +509,6 @@ let load_main dirname section =
running_provers_max = get_int ~default:default_main.running_provers_max running_provers_max = get_int ~default:default_main.running_provers_max
section "running_provers_max"; section "running_provers_max";
plugins = get_stringl ~default:[] section "plugin"; plugins = get_stringl ~default:[] section "plugin";
cntexample = get_bool ~default:default_main.cntexample section "get-ce"
} }
let read_config_rc conf_file = let read_config_rc conf_file =
......
...@@ -75,7 +75,6 @@ val loadpath: main -> string list ...@@ -75,7 +75,6 @@ val loadpath: main -> string list
val timelimit: main -> int val timelimit: main -> int
val memlimit: main -> int val memlimit: main -> int
val running_provers_max: main -> int val running_provers_max: main -> int
val cntexample: main -> bool
val set_limits: main -> int -> int -> int -> main val set_limits: main -> int -> int -> int -> main
val plugins : main -> string list val plugins : main -> string list
......
...@@ -977,7 +977,6 @@ let () = Queue.iter (open_file ~start:true) files ...@@ -977,7 +977,6 @@ let () = Queue.iter (open_file ~start:true) files
let prover_on_selected_goals pr = let prover_on_selected_goals pr =
let timelimit = gconfig.session_time_limit in let timelimit = gconfig.session_time_limit in
let memlimit = gconfig.session_mem_limit in let memlimit = gconfig.session_mem_limit in
let cntexample = Whyconf.cntexample (Whyconf.get_main gconfig.config) in
List.iter List.iter
(fun row -> (fun row ->
try try
......
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