Commit 55b2c6f6 authored by MARCHE Claude's avatar MARCHE Claude

remove warning new in ocaml 4.02.3 : ocamldoc comment (** .. *) not attached correctly

parent 6bb8e924
......@@ -60,7 +60,7 @@ let scanf s =
(** the main function *)
let read_channel env path filename cin =
(** Find the int theory and the needed operation *)
(* Find the int theory and the needed operation *)
let th_int = Env.read_theory env ["int"] "Int" in
let leq = ns_find_ls th_int.th_export ["infix <"] in
let plus_symbol = Theory.ns_find_ls th_int.Theory.th_export ["infix +"] in
......@@ -73,7 +73,7 @@ let read_channel env path filename cin =
t_app_infer neg_symbol [t_nat_const (-n)]
in
(** create a contraint : polynome <= constant *)
(* create a contraint : polynome <= constant *)
let create_lit lvar k lits _ =
let left = List.fold_left (fun acc e ->
let const = (Random.int k) - (k/2) in
......@@ -83,7 +83,7 @@ let read_channel env path filename cin =
let rconst = (Random.int k) - (k/2) in
t_and_simp lits (t_app leq [left;t_int_const rconst] None) in
(** create a set of constraints *)
(* create a set of constraints *)
let create_fmla nvar m k =
let lvar = Util.mapi (fun _ -> create_vsymbol (id_fresh "x") Ty.ty_int)
1 nvar in
......@@ -91,7 +91,7 @@ let read_channel env path filename cin =
let lits = Util.foldi (create_lit lt k) t_true 1 m in
t_forall_close lvar [] (t_implies_simp lits t_false) in
(** read the first line *)
(* read the first line *)
let line = ref 0 in
begin try
let seed = input_line cin in
......@@ -100,16 +100,16 @@ let read_channel env path filename cin =
Printf.eprintf "error file %s line 1\n" filename;
exit 1
end;
(** Create the theory *)
(* Create the theory *)
let th_uc_loc = Loc.user_position filename 1 0 0 in
let th_uc = create_theory ~path (id_user "EqLin" th_uc_loc) in
let th_uc = Theory.use_export th_uc th_int in
(** Read one line and add it to the theory *)
(* Read one line and add it to the theory *)
let fold th_uc s =
let nvar,m,k =
try
incr line;
(** Dont use scanf because I don't know how to link it in plugin
(* Dont use scanf because I don't know how to link it in plugin
(without segfault) *)
(* Scanf.sscanf s "%i %i %i" (fun nvar m k -> nvar,m,k) *)
scanf s
......@@ -120,9 +120,9 @@ let read_channel env path filename cin =
let fmla = create_fmla nvar m k in
let th_uc = Theory.add_prop_decl th_uc Decl.Pgoal goal_id fmla in
th_uc in
(** Read all the file *)
(* Read all the file *)
let th_uc = Sysutil.fold_channel fold th_uc cin in
(** Return the map with the theory *)
(* Return the map with the theory *)
Mstr.singleton "EquLin" (close_theory th_uc)
let () = Env.register_format Env.base_language "equlin" ["equlin"] read_channel
......
......@@ -88,7 +88,7 @@ let load_prover kind (id,section) =
prover_id = id;
prover_name = get_string section "name";
prover_altern = get_string section ~default:"" "alternative";
compile_time_support =
compile_time_support =
get_bool section ~default:false "compile_time_support";
execs = get_stringl section "exec";
version_switch = get_string section ~default:"" "version_switch";
......@@ -148,16 +148,16 @@ end)
type env =
{
(** memoization of (exec_name,version_switch)
(* memoization of (exec_name,version_switch)
-> Some output | None doesn't exists *)
prover_output : string option Hstr2.t;
(** existing executable table:
(* existing executable table:
exec_name -> | Some (priority, id, prover_config)
unknown version (neither good or bad)
| None there is a good version *)
prover_unknown_version :
(int * string * config_prover) option Hstr.t;
(** string -> priority * prover *)
(* string -> priority * prover *)
prover_shortcuts : (int * prover) Hstr.t;
mutable possible_prover_shortcuts : (filter_prover * string) list;
}
......@@ -285,13 +285,13 @@ let find_prover_altern provers prover_id =
if Mprover.mem prover_id_n provers
then aux (n+1)
else prover_id_n in
(** start with 2 in order to have toto_alt, toto_alt2,
toto_alt3,... and not toto_alt, toto_alt1 which can be
confusing *)
(* start with 2 in order to have toto_alt, toto_alt2,
toto_alt3,... and not toto_alt, toto_alt1 which can be
confusing *)
aux 2
let add_prover_with_uniq_id prover provers =
(** find an unique prover triplet *)
(* find an unique prover triplet *)
let prover_id = find_prover_altern provers prover.Wc.prover in
let prover = {prover with Wc.prover = prover_id} in
Mprover.add prover_id prover provers
......@@ -330,20 +330,20 @@ let detect_exec env main data acc exec_name =
""
end
in
(** bad mean here not good, it's not the same thing than a version
of a prover with known problems *)
(* bad mean here not good, it's not the same thing than a version
of a prover with known problems *)
let bad = List.exists (check_version ver) data.versions_bad in
if bad then (known_version env exec_name; acc)
else
(* check if this prover needs compile-time support *)
let missing_compile_time_support =
if data.compile_time_support then
try
try
let compile_time_ver =
List.assoc data.prover_name Config.compile_time_support
in
List.assoc data.prover_name Config.compile_time_support
in
if compile_time_ver <> ver then begin
eprintf
eprintf
"Found prover %s version %s, but Why3 was compiled with support for version %s@."
data.prover_name ver compile_time_ver;
true
......@@ -351,7 +351,7 @@ let detect_exec env main data acc exec_name =
else
false
with Not_found ->
eprintf
eprintf
"Found prover %s version %s, but Why3 wasn't compiled with support for it@."
data.prover_name ver;
true
......@@ -364,7 +364,7 @@ let detect_exec env main data acc exec_name =
let old = List.exists (check_version ver) data.versions_old in
match data.prover_command with
| None ->
(** Empty prover *)
(* Empty prover *)
if good || old then begin (** Known version with error *)
known_version env exec_name;
eprintf "Found prover %s version %s%s@."
......@@ -374,10 +374,10 @@ let detect_exec env main data acc exec_name =
data.message);
acc
end
else (** it's not a known bad version *) acc
else (* it's not a known bad version *) acc
| Some prover_command ->
(** create the prover config *)
(* create the prover config *)
let c = make_command exec_name prover_command in
let c_steps = (match data.prover_command_steps with
| None -> None
......@@ -425,10 +425,10 @@ let detect_unknown env detected =
Warning.emit "Warning: prover %s version %s is not known to be \
supported.@."
prover.Wc.prover_name prover.prover_version;
(** Pb: Even if it match the first prover section (normally
highest priority) since it is unknown it has the lower
priority for its id as shortcut. Perhaps we don't want
that. *)
(* Pb: Even if it match the first prover section (normally
highest priority) since it is unknown it has the lower
priority for its id as shortcut. Perhaps we don't want
that. *)
add_id_prover_shortcut env prover_id prover priority;
add_prover_with_uniq_id prover_config acc)
env.prover_unknown_version detected
......@@ -500,7 +500,7 @@ let add_prover_binary config id path =
Loc.errorm "File %s does not correspond to the prover id %s" path id;
let provers = get_provers config in
let fold _ p provers =
(** find a prover altern not used *)
(* find a prover altern not used *)
(* Is a prover with this name and version already in config? *)
let prover_id =
if not (Mprover.mem p.prover provers) then p.prover else
......
......@@ -34,7 +34,7 @@ let magicnumber = 14
exception WrongMagicNumber
let why3_regexp_of_string s = (** define a regexp in why3 *)
let why3_regexp_of_string s = (* define a regexp in why3 *)
if s = "" then Str.regexp "^$" else
if s.[0] = '^' then Str.regexp s else
Str.regexp ("^" ^ Str.quote s ^ "$")
......@@ -323,15 +323,15 @@ let set_prover_shortcuts rc shortcuts =
set_simple_family rc "shortcut" family
let set_provers_shortcuts rc shortcuts provers =
(** inverse the shortcut map *)
(* inverse the shortcut map *)
let shortcuts = Mstr.fold (fun shortcut prover acc ->
Mprover.change (function
| None -> Some [shortcut]
| Some l -> Some (shortcut::l)) prover acc) shortcuts Mprover.empty in
(** the shortcut to unknown prover *)
(* the shortcut to unknown prover *)
let shortcuts_prover_unknown = Mprover.set_diff shortcuts provers in
let rc = set_prover_shortcuts rc shortcuts_prover_unknown in
(** merge the known *)
(* merge the known *)
let _,shortcuts_provers_known =
Mprover.mapi_fold (fun k v acc ->
let acc = Mprover.next_ge_enum k acc in
......@@ -664,7 +664,7 @@ let merge_config config filename =
Format.eprintf "[Config] reading extra configuration file %s@." filename;
let dirname = get_dirname filename in
let rc = Rc.from_file filename in
(** modify main *)
(* modify main *)
let main = match get_section rc "main" with
| None -> config.main
| Some rc ->
......@@ -678,7 +678,7 @@ let merge_config config filename =
let strategies =
List.fold_left load_strategy config.strategies more_strategies
in
(** modify provers *)
(* modify provers *)
let create_filter_prover section =
try
let name = get_string section "name" in
......@@ -692,7 +692,7 @@ let merge_config config filename =
let prover_modifiers = get_simple_family rc "prover_modifiers" in
let prover_modifiers =
List.map (fun sec -> create_filter_prover sec, sec) prover_modifiers in
(** add provers *)
(* add provers *)
let provers = List.fold_left
(fun provers (fp, section) ->
Mprover.mapi (fun p c ->
......@@ -709,7 +709,7 @@ let merge_config config filename =
let provers,shortcuts =
List.fold_left (load_prover dirname)
(provers,config.prover_shortcuts) (get_simple_family rc "prover") in
(** modify editors *)
(* modify editors *)
let editor_modifiers = get_family rc "editor_modifiers" in
let editors = List.fold_left
(fun editors (id, section) ->
......@@ -719,7 +719,7 @@ let merge_config config filename =
let opt = get_stringl ~default:[] section "option" in
Some { c with editor_options = opt @ c.editor_options }) id editors
) config.editors editor_modifiers in
(** add editors *)
(* add editors *)
let editors = List.fold_left load_editor editors (get_family rc "editor") in
{ config with main = main; provers = provers; strategies = strategies;
prover_shortcuts = shortcuts; editors = editors }
......
......@@ -21,7 +21,7 @@ let () = (***** TODO TODO make that work, it seems not called!!! *)
let why3_handler exn =
Format.eprintf "@[Why3ide callback raised an exception:@\n%a@]@.@."
Exn_printer.exn_printer exn;
(** print the stack trace if asked to (can't be done by the usual way) *)
(* print the stack trace if asked to (can't be done by the usual way) *)
if Debug.test_flag Debug.stack_trace then
Printf.eprintf "Backtrace:\n%t\n%!" Printexc.print_backtrace
in
......@@ -283,7 +283,7 @@ let incr_font_size n =
*)
let image_default = ref (GdkPixbuf.create ~width:1 ~height:1 ())
(** dumb pixbuf *)
(* dumb pixbuf *)
let image_undone = ref !image_default
let image_scheduled = ref !image_default
let image_running = ref !image_default
......@@ -1026,17 +1026,17 @@ let preferences (c : t) =
in
let vbox = dialog#vbox in
let notebook = GPack.notebook ~packing:vbox#add () in
(** page "general settings" **)
(* page "general settings" **)
general_settings c notebook;
(** page "appearance" **)
(* page "appearance" **)
appearance_settings c notebook;
(*** page "editors" **)
(* page "editors" **)
editors_page c notebook;
(** page "Provers" **)
(* page "Provers" **)
provers_page c notebook;
(*** page "uninstalled provers" *)
(* page "uninstalled provers" *)
alternatives_frame c notebook;
(** page "Colors" **)
(* page "Colors" **)
(*
let label2 = GMisc.label ~text:"Colors" () in
let _color_sel = GMisc.color_selection (* ~title:"Goal color" *)
......@@ -1050,7 +1050,7 @@ let preferences (c : t) =
c)
in
*)
(** bottom button **)
(* bottom button **)
dialog#add_button "Save&Close" `SAVE ;
dialog#add_button "Close" `CLOSE ;
let ( answer : [`SAVE | `CLOSE | `DELETE_EVENT ]) = dialog#run () in
......
......@@ -828,11 +828,11 @@ let project_dir =
in
Debug.dprintf debug
"[GUI] using '%s' as directory for the project@." d;
Queue.push fname files; (** we need to open [fname] *)
Queue.push fname files; (* we need to open [fname] *)
d
end
else begin
(** The first argument is not a directory and it's not the
(* The first argument is not a directory and it's not the
only file *)
Format.eprintf
"[Error] @[When@ more@ than@ one@ file@ is@ given@ on@ the@ \
......@@ -1082,7 +1082,7 @@ let bisect_proof_attempt pa =
dprintf debug "Bisecting interrupted.@."
| S.Unedited | S.JustEdited -> assert false
| S.InternalFailure exn ->
(** Perhaps the test can be considered false in this case? *)
(* Perhaps the test can be considered false in this case? *)
dprintf debug "Bisecting interrupted by an error %a.@."
Exn_printer.exn_printer exn
| S.Done res ->
......@@ -1119,16 +1119,16 @@ let bisect_proof_attempt pa =
~memlimit:pa.S.proof_memlimit
~steplimit:(-1)
?old:(S.get_edited_as_abs eS.S.session pa)
(** It is dangerous, isn't it? to be in place for bisecting? *)
(* It is dangerous, isn't it? to be in place for bisecting? *)
~inplace:lp.S.prover_config.C.in_place
~command:(C.get_complete_command lp.S.prover_config (-1))
~driver:lp.S.prover_driver
~callback:(callback lp pa c) sched t
in
(** Run once the complete goal in order to verify its validity and
update the proof attempt *)
(* Run once the complete goal in order to verify its validity and
update the proof attempt *)
let first_callback pa = function
(** this pa can be different than the first pa *)
(* this pa can be different than the first pa *)
| S.Running | S.Scheduled -> ()
| S.Interrupted ->
dprintf debug "Bisecting interrupted.@."
......@@ -2036,10 +2036,10 @@ let reload () =
try
erase_color_loc source_view;
current_file := "";
(** create a new environnement
(in order to reload the files which are "use") *)
(* create a new environnement
(in order to reload the files which are "use") *)
gconfig.env <- Env.create_env (Env.get_loadpath gconfig.env);
(** reload the session *)
(* reload the session *)
let old_session = (env_session()).S.session in
let new_env_session,(_:bool),(_:bool) =
(* use_shapes is true since session is in memory *)
......
......@@ -430,7 +430,7 @@ let read_comment =
let end_comment = Str.regexp ".*\\*)" in
fun ch ->
let line = ref "" in
(** look for "( * name" *)
(* look for "( * name" *)
let name =
try
while true do
......@@ -442,7 +442,7 @@ let read_comment =
done;
assert false
with StringValue name -> name in
(** look for end of comment *)
(* look for end of comment *)
while not (Str.string_match end_comment (!line) 0) do
line := input_line ch
done;
......@@ -828,9 +828,9 @@ let print_equivalence_lemma ~old info fmt ((ls,_) as d) =
(print_equivalence_lemma ~prev info fmt name d; forget_tvs ())
let print_logic_decl ~old info fmt d =
(** During realization the definition of a "builtin" symbol is
printed and an equivalence lemma with associated coq function is
requested *)
(* During realization the definition of a "builtin" symbol is
printed and an equivalence lemma with associated coq function is
requested *)
if not (Mid.mem (fst d).ls_name info.info_syn) then
(print_logic_decl info fmt d; forget_tvs ())
else if info.realization then
......
......@@ -27,16 +27,16 @@ let ident_printer =
"funs";"extrafuns";"extrasorts";"extrapreds";"language";
"notes";"preds";"sorts";"status";"theory";"Int";"Real";"Bool";
"Array";"U";"select";"store"]*)
(** smtlib2 V2 p71 *)
[(** General: *)
(* smtlib2 V2 p71 *)
[(* General: *)
"!";"_"; "as"; "DECIMAL"; "exists"; "forall"; "let"; "NUMERAL";
"par"; "STRING";
(**Command names:*)
(* Command names: *)
"assert";"check-sat"; "declare-sort";"declare-fun";"define-sort";
"define-fun";"exit";"get-assertions";"get-assignment"; "get-info";
"get-option"; "get-proof"; "get-unsat-core"; "get-value"; "pop"; "push";
"set-logic"; "set-info"; "set-option";
(** for security *)
(* for security *)
"BOOLEAN";"unsat";"sat";"TRUE";"FALSE";
"TRUE";"CHECK";"QUERY";"ASSERT";"TYPE";"SUBTYPE"]
in
......
......@@ -326,9 +326,9 @@ let print_logic_decl info fmt ((ls, _) as d) =
forget_tvs ()
let print_logic_decl info fmt d =
(** During realization the definition of a "builtin" symbol is
printed and an equivalence lemma with associated Isabelle function is
requested *)
(* During realization the definition of a "builtin" symbol is
printed and an equivalence lemma with associated Isabelle function is
requested *)
if not (Mid.mem (fst d).ls_name info.info_syn) then
print_logic_decl info fmt d
else if info.realization then
......
......@@ -32,23 +32,23 @@ let ident_printer =
"funs";"extrafuns";"extrasorts";"extrapreds";"language";
"notes";"preds";"sorts";"status";"theory";"Int";"Real";"Bool";
"Array";"U";"select";"store"]*)
(** smtlib2 V2 p71 *)
[(** Base SMT-LIB tokens *)
(* smtlib2 V2 p71 *)
[(* Base SMT-LIB tokens *)
"assert"; "check-sat"; "declare-fun"; "declare-sort"; "define-fun";
"define-sort"; "get-value"; "get-assignment"; "get-assertions";
"get-proof"; "get-unsat-core"; "exit"; "ite"; "let"; "!"; "_";
"set-logic"; "set-info"; "get-info"; "set-option"; "get-option";
"push"; "pop"; "as";
(** extended commands *)
(* extended commands *)
"declare-datatypes"; "get-model"; "echo"; "assert-rewrite";
"assert-reduction"; "assert-propagation"; "declare-sorts";
"declare-funs"; "declare-preds"; "define"; "declare-const";
"simplify";
(** attributes *)
(* attributes *)
(** operators, including theory symbols *)
(* operators, including theory symbols *)
"and"; "distinct"; "exists"; "forall"; "is_int"; "not"; "or"; "select";
"store"; "to_int"; "to_real"; "xor";
......@@ -62,7 +62,7 @@ let ident_printer =
"cos"; "sin"; "tan"; "atan"; "pi";
(** Other stuff that Why3 seems to need *)
(* Other stuff that Why3 seems to need *)
"DECIMAL"; "NUMERAL"; "par"; "STRING";
"unsat";"sat";
"Bool"; "true"; "false";
......@@ -70,7 +70,7 @@ let ident_printer =
"abs";
"BitVec"; "extract"; "bv2nat"; "nat2bv";
(** From Z3 *)
(* From Z3 *)
"map"; "bv"; "subset"; "union"
]
in
......
......@@ -27,16 +27,16 @@ let ident_printer =
"funs";"extrafuns";"extrasorts";"extrapreds";"language";
"notes";"preds";"sorts";"status";"theory";"Int";"Real";"Bool";
"Array";"U";"select";"store"]*)
(** smtlib2 V2 p71 *)
[(** General: *)
(* smtlib2 V2 p71 *)
[(* General: *)
"!";"_"; "as"; "DECIMAL"; "exists"; "forall"; "let"; "NUMERAL";
"par"; "STRING"; "if"; "ite";
(**Command names:*)
(* Command names: *)
"define";
"define-type";"exit";"get-assertions";"get-assignment"; "get-info";
"get-option"; "get-proof"; "get-unsat-core"; "get-value"; "pop"; "push";
"set-logic"; "set-info"; "set-option";
(** for security *)
(* for security *)
"bool";"unsat";"sat";"true";"false";
"true";"check";"assert";"TYPE";"SUBTYPE";
"scalar";"select";"update";"int";"real";"nat";
......
......@@ -89,7 +89,7 @@ module Mmeta_args = Extmap.Make(struct
let compare_meta_arg x y =
match x,y with
(** These hash are in fact tag *)
(* These hash are in fact tag *)
| MAty x, MAty y -> compare (ty_hash x) (ty_hash y)
| MAts x, MAts y -> compare (ts_hash x) (ts_hash y)
| MAls x, MAls y -> compare (ls_hash x) (ls_hash y)
......@@ -404,9 +404,9 @@ module PTreeT = struct
| Session s ->
let l = ref [] in
session_iter (fun a -> l := (Any a)::!l) s;
(** Previously "" was `Filename.basename s.session_dir` but
the tree depend on the filename given in input and not the content
which is not easy for diffing
(* Previously "" was `Filename.basename s.session_dir` but
the tree depend on the filename given in input and not the content
which is not easy for diffing
*)
"",!l
......@@ -664,7 +664,7 @@ and save_metas ctxt fmt _ m =
save_string ts.ts_name.id_string (List.length ts.ts_args)
(ts_hash ts) save_pos pos in
let save_ls_pos fmt ls pos =
(** TODO: add the signature? *)
(* TODO: add the signature? *)
fprintf fmt "@\n@[<hov 1><ls_pos@ name=\"%a\"@ id=\"%i\"@ %a@]@\n</ls_pos>"
save_string ls.ls_name.id_string
(ls_hash ls) save_pos pos
......@@ -1137,7 +1137,7 @@ let int_attribute field r =
try
int_of_string (List.assoc field r.Xml.attributes)
with Not_found | Invalid_argument _ ->
(** TODO: use real error *)
(* TODO: use real error *)
eprintf "[Error] missing required attribute '%s' from element '%s'@."
field r.Xml.name;
assert false
......@@ -1307,7 +1307,7 @@ and load_proof_or_transf ctxt mg a =
[] a.Xml.elements);
(* already done by raw_add_transformation:
Hashtbl.add mg.transformations trname mtr *)
(** The attribute "proved" is required but not read *)
(* The attribute "proved" is required but not read *)
mtr.transf_verified <- transf_verified mtr
| "metas" -> load_metas ctxt mg a;
| "label" -> ()
......@@ -1349,7 +1349,7 @@ and load_metas ctxt mg a =
let idpos_ts = Mts.add ts pos idpos.idpos_ts in
{ idpos with idpos_ts = idpos_ts }
| "ls_pos" ->
(** TODO signature? *)
(* TODO signature? *)
let ls = Term.create_lsymbol (Ident.id_fresh name) [] None in
Hint.add hls intid ls;
let idpos_ls = Mls.add ls pos idpos.idpos_ls in
......@@ -1427,7 +1427,7 @@ and load_metas ctxt mg a =
List.hd (load_goal ctxt (Parent_metas metas) [] goal);
(* already done by raw_add_transformation:
Hashtbl.add mg.transformations trname mtr *)
(** The attribute "proved" is required but not read *)
(* The attribute "proved" is required but not read *)
metas.metas_verified <- metas_verified metas
......@@ -1467,7 +1467,7 @@ let load_file ~keygen session old_provers f =
mf.file_verified <- file_verified mf;
old_provers
| "prover" ->
(** The id is just for the session file *)
(* The id is just for the session file *)
let id = string_attribute "id" f in
begin
try
......@@ -1495,7 +1495,7 @@ let load_session ~keygen session xml =
let shape_version = int_attribute_def "shape_version" xml 1 in
session.session_shape_version <- shape_version;
Debug.dprintf debug "[Info] load_session: shape version is %d@\n" shape_version;
(** just to keep the old_provers somewhere *)
(* just to keep the old_provers somewhere *)
let old_provers =
List.fold_left (load_file ~keygen session) Mint.empty xml.Xml.elements
in
......@@ -1619,7 +1619,7 @@ let read_session_with_keys ~keygen dir =
let xml_filename = Filename.concat dir db_filename in
let session = empty_session dir in
let use_shapes =
(** If the xml is present we read it, otherwise we consider it empty *)
(* If the xml is present we read it, otherwise we consider it empty *)
if Sys.file_exists xml_filename then
try
Tc.reset_dict ();
......@@ -1681,7 +1681,7 @@ let read_file env ?format fn =
let ltheories =
Mstr.fold
(fun name th acc ->
(** Hack : with WP [name] and [th.Theory.th_name.Ident.id_string] *)
(* Hack : with WP [name] and [th.Theory.th_name.Ident.id_string] *)
let th_name =
Ident.id_register (Ident.id_derive name th.Theory.th_name) in
match th.Theory.th_name.Ident.id_loc with
......@@ -1850,7 +1850,7 @@ let add_registered_metas ~keygen env added0 g =
let add_meta task (s,l) =
let m = Theory.lookup_meta s in
Task.add_meta task m l in
(** add before the goal *)
(* add before the goal *)
let task = List.fold_left add_meta task0 added0 in
let task = add_tdecl task goal in
let idpos = pos_of_metas added0 in
......@@ -1923,16 +1923,16 @@ let copy_external_proof
let nprover = match prover with
| None -> a.proof_prover
| Some prover -> prover in
(** copy or generate the edit file if needed *)
(* copy or generate the edit file if needed *)
let edit =
match edit, a.proof_edited_as, session with
| Some edit, _, _ -> edit
| _, None, _ -> None
| _, _, None -> (** In the other case a session is needed *)
| _, _, None -> (* In the other case a session is needed *)
None
| _, Some file, Some session ->
assert (file != "");
(** Copy the edited file *)
(* Copy the edited file *)
let dir = session.session_dir in
let file = Filename.concat dir file in
if not (Sys.file_exists file) then None else
......@@ -1943,7 +1943,7 @@ let copy_external_proof
let dst_file = Sysutil.relativize_filename dir dst_file in
Some dst_file
| (_, _, None,_)| (_, _, _, None) ->
(** In the other cases an env_session and a task are needed *)
(* In the other cases an env_session and a task are needed *)
None
| _, _, Some task, Some env_session ->
match load_prover env_session nprover with
......@@ -2078,11 +2078,11 @@ exception Pr_not_found of prsymbol
let merge_metas_in_task ~theories env task from_metas =
(** Find in the new task the new symbol (ts,ls,pr) *)
(** We order the position bottom up and find the ident as we go
through the task *)
(* Find in the new task the new symbol (ts,ls,pr) *)
(* We order the position bottom up and find the ident as we go
through the task *)
(** hashtbl that will contain the conversion *)
(* hashtbl that will contain the conversion *)
let hts = Hts.create 4 in
let hls = Hls.create 4 in
let hpr = Hpr.create 10 in
......@@ -2137,7 +2137,7 @@ let merge_metas_in_task ~theories env task from_metas =
meta_name
(Pp.print_list Pp.space Pretty.print_meta_arg) meta_args in
(** Now convert the metas to the new symbol *)
(* Now convert the metas to the new symbol *)
let add_meta ((metas,task) as acc) meta_name meta_args =
let conv_ts ts = Hts.find_exn hts (Ts_not_found ts) ts in
let conv_ls ls = Hls.find_exn hls (Ls_not_found ls) ls in
......@@ -2221,9 +2221,9 @@ type 'key update_context =
let rec recover_sub_tasks ~theories env_session task g =
g.goal_task <- Some task;
(** Check that the sum and shape don't change (the order is kept)
It seems an acceptable limitation. Non-deterministic transformation seems
ugly.
(* Check that the sum and shape don't change (the order is kept)
It seems an acceptable limitation. Non-deterministic transformation seems
ugly.
*)
let version = env_session.session.session_shape_version in
let sum = Termcode.task_checksum ~version task in
......@@ -2241,8 +2241,8 @@ let rec recover_sub_tasks ~theories env_session task g =
Mmetas_args.iter (fun _ t ->
let task,_metas,_to_idpos,_obsolete =
merge_metas_in_task ~theories env_session task t in
(** It is better to keep the original metas and idpos *)
(** If it is obsolete the next task will see it *)
(* It is better to keep the original metas and idpos *)
(* If it is obsolete the next task will see it *)
recover_sub_tasks ~theories env_session task t.metas_goal
) g.goal_metas
......@@ -2595,14 +2595,14 @@ and add_metas_to_goal ~keygen env to_goal from_metas =
from_metas.metas_added from_metas.metas_idpos
in
let goal,task0 = Task