Commit 1a748647 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove incorrect ocamldoc comments.

parent 189b4988
......@@ -410,17 +410,17 @@ module Select = struct
| _ -> failwith "bad literal in the goal clause" in
let l0 = List.fold_left add_literal Sexpr.empty goal_clause in
(** explore one more step *)
(* explore one more step *)
let rec one_step cur =
let step = Sexpr.fold explore cur [cur;cur] in
Format.eprintf "one step made !@.";
step
(** explores the neighbours of [vertex] *)
(* explores the neighbours of [vertex] *)
and explore vertex l = match l with [_next_cur;cur] ->
(** [changed] indicates whether a vertex has been added;
[v] is a vertex *)
(* [changed] indicates whether a vertex has been added;
[v] is a vertex *)
let find_odd v ((acc,_changed) as old) =
if Sexpr.mem v acc then old else
let count = GC.fold_pred
......@@ -442,7 +442,7 @@ module Select = struct
| _ -> assert false (*only not to have warnings on non-exhaustive match*)
(** iterates [one_step] until an exception is raised *)
(* iterates [one_step] until an exception is raised *)
and control cur acc =
let next_acc = try
let next_step = one_step cur in
......
......@@ -233,7 +233,6 @@ val why3_regexp_of_string : string -> Str.regexp
(** {2 For accesing other parts of the configuration } *)
(** Access to the Rc.t *)
val get_section : config -> string -> Rc.section option
(** [get_section config name] Same as {!Rc.get_section} except name
must not be "main" *)
......
......@@ -77,7 +77,7 @@ let model_vc_term_label = Ident.create_label "model_vc"
(* This label identifies the term that triggers the VC. *)
let add_model_element (el: term) info_model =
(** Add element el (term) to info_model.
(* Add element el (term) to info_model.
If an element with the same hash (the same set of labels + the same
location) as the element el already exists in info_model, replace it with el.
......
......@@ -63,7 +63,7 @@ let ident_printer () =
"cos"; "sin"; "tan"; "atan"; "pi";
(** the new floating point theory - updated to the 2014-05-27 standard *)
(* the new floating point theory - updated to the 2014-05-27 standard *)
"FloatingPoint"; "fp";
"Float16"; "Float32"; "Float64"; "Float128";
"RoundingMode";
......@@ -82,7 +82,7 @@ let ident_printer () =
"to_fp"; "to_fp_unsigned";
"fp.to_ubv"; "fp.to_sbv"; "fp.to_real";
(** the new proposed string theory *)
(* the new proposed string theory *)
"String";
"str.++"; "str.len"; "str.substr"; "str.contains"; "str.at";
"str.indexof"; "str.prefixof"; "str.suffixof"; "int.to.str";
......@@ -90,14 +90,14 @@ let ident_printer () =
"str.in.re"; "str.to.re"; "re.++"; "re.union"; "re.inter";
"re.*"; "re.+"; "re.opt"; "re.range"; "re.loop";
(** the new proposed set theory *)
(* the new proposed set theory *)
"union"; "intersection"; "setminus"; "subset"; "member";
"singleton"; "insert";
(** built-in sorts *)
(* built-in sorts *)
"Bool"; "Int"; "Real"; "BitVec"; "Array";
(** Other stuff that Why3 seems to need *)
(* Other stuff that Why3 seems to need *)
"DECIMAL"; "NUMERAL"; "par"; "STRING";
"unsat";"sat";
"true"; "false";
......
......@@ -277,8 +277,8 @@ module Make(O: OBSERVER) : sig
'valid' *)
val check_all:
?release:bool -> (** Can all the goals be released at the end? def: false *)
use_steps:bool -> (** Replay use recorded number of proof steps *)
?release:bool -> (* Can all the goals be released at the end? def: false *)
use_steps:bool -> (* Replay use recorded number of proof steps *)
?filter:(O.key proof_attempt -> bool) ->
O.key env_session -> t ->
callback:
......
......@@ -64,7 +64,7 @@ let timestamp = register_info_flag "timestamp"
let time_start = Unix.gettimeofday ()
let set_debug_formatter f =
(** enable the usual behavior of stderr: flush at every new line *)
(* enable the usual behavior of stderr: flush at every new line *)
let o = Format.pp_get_formatter_out_functions f () in
Format.pp_set_formatter_out_functions f
{ o with Format.out_newline =
......@@ -178,9 +178,10 @@ module Stats = struct
let () = at_exit (fun () ->
print ();
Format.pp_print_flush !formatter ())
(** SIGXCPU cpu time limit reached *)
(** SIGXCPU cpu time limit reached *)
let _ =
(** TODO? have a possible callback for printing different message*)
(* TODO? have a possible callback for printing different message*)
Sys.signal Sys.sigint (Sys.Signal_handle (fun _ -> exit 2))
let register ~print ~name ~init =
......
......@@ -169,7 +169,7 @@ module Make (S : Weakey) = struct
let tbl_final t =
tbl_final_aux t;
(** We don't need anymore the weak hashset, we can release it *)
(* We don't need anymore the weak hashset, we can release it *)
Hashtbl.remove gen_table t.tbl_tag
(** All the hashweak that can be collected. When a hashweak is
......
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