From 6d9f54944a1c3f792662f9e48b66d924f1a3be3e Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 13 Mar 2023 14:33:45 +0100 Subject: [PATCH] Fix JS worker --- src/bin/common/solving_loop.ml | 14 +- src/bin/gui/annoted_ast.ml | 2 +- src/bin/js/worker_js.ml | 496 +++++++++++---------- src/bin/text/main_text.ml | 4 +- src/lib/reasoners/adt_rel.ml | 2 +- src/lib/reasoners/enum_rel.ml | 4 +- src/lib/reasoners/fun_sat.ml | 4 +- src/lib/reasoners/intervalCalculus.ml | 16 +- src/lib/reasoners/satml_frontend_hybrid.ml | 2 +- src/lib/reasoners/theory.ml | 4 +- src/lib/structures/ty.mli | 2 +- 11 files changed, 278 insertions(+), 272 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 0cf9248ee7..fc7e470bed 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -270,11 +270,11 @@ let main () = in (* let all_used_context = FE.init_all_used_context () in - if Options.get_timelimit_per_goal() then - FE.print_status FE.Preprocess 0; - let assertion_stack = Stack.create () in - let typing_loop state p = - if get_parse_only () then state else begin + if Options.get_timelimit_per_goal() then + FE.print_status FE.Preprocess 0; + let assertion_stack = Stack.create () in + let typing_loop state p = + if get_parse_only () then state else begin try let l, env = I.type_parsed state.env assertion_stack p in let used_names = I.get_env_logics state.env in @@ -285,8 +285,8 @@ let main () = if e != Warning_as_error then Printer.print_err "%a" Errors.report e; exit 1 - end - in *) + end + in *) let handle_stmt : FE.used_context -> State.t -> diff --git a/src/bin/gui/annoted_ast.ml b/src/bin/gui/annoted_ast.ml index 1dcb4b8928..8a4c37d64a 100644 --- a/src/bin/gui/annoted_ast.ml +++ b/src/bin/gui/annoted_ast.ml @@ -1841,7 +1841,7 @@ let rec add_atyped_decl errors (buffer:sbuffer) ?(indent=0) ?(tags=[]) d = | _ -> AFop (AOPnot, [aaform]) in let goal_str = - match (gs : Typed.goal_sort) with + match (gs : Ty.goal_sort) with | Thm -> "check valid" | Sat -> "check sat" | AllSat l -> diff --git a/src/bin/js/worker_js.ml b/src/bin/js/worker_js.ml index 5e391761bd..8cdb73d93a 100644 --- a/src/bin/js/worker_js.ml +++ b/src/bin/js/worker_js.ml @@ -107,7 +107,8 @@ let main worker_id content = let _,_,dep = List.fold_left (FE.process_decl - get_status_and_print used_context consistent_dep_stack) + get_status_and_print used_context Util.SS.empty + consistent_dep_stack) (SAT.empty_with_inst add_inst, true, Explanation.empty) cnf in if Options.get_unsat_core () then begin @@ -124,7 +125,8 @@ let main worker_id content = begin match kind with | Ty.Check | Ty.Cut -> { state with local = []; } - | Ty.Thm | Ty.Sat -> { state with global = []; local = []; } + | Ty.Thm | Ty.Sat | Ty.AllSat _ -> + { state with global = []; local = []; } end | Typed.TAxiom (_, s, _, _) when Ty.is_global_hyp s -> let cnf = Cnf.make state.global td in @@ -210,252 +212,254 @@ let main worker_id content = ) tbl [] in - let get_status_and_print status n = - returned_status := - begin match status with - | FE.Unsat _ -> Worker_interface.Unsat n - | FE.Inconsistent _ -> Worker_interface.Inconsistent n - | FE.Sat _ -> Worker_interface.Sat n - | FE.Unknown _ -> Worker_interface.Unknown n - | FE.Timeout _ -> Worker_interface.LimitReached "timeout" - | FE.Preprocess -> Worker_interface.Unknown n - end; - FE.print_status status n - in - - let solve all_context (cnf, goal_name) = - let used_context = FE.choose_used_context all_context ~goal_name in - let consistent_dep_stack = Stack.create () in - SAT.reset_refs (); - let _,_,dep = - List.fold_left - (FE.process_decl - get_status_and_print used_context consistent_dep_stack) - (SAT.empty_with_inst add_inst, true, Explanation.empty) cnf in - - if Options.get_unsat_core () then begin - unsat_core := Explanation.get_unsat_core dep; - end; - in - - let typed_loop all_context state td = - match td.Typed.c with - | Typed.TGoal (_, kind, name, _) -> - let l = state.local @ state.global @ state.ctx in - let cnf = List.rev @@ Cnf.make l td in - let () = solve all_context (cnf, name) in - begin match kind with - | Typed.Check - | Typed.Cut -> { state with local = []; } - | _ -> { state with global = []; local = []; } - end - | Typed.TAxiom (_, s, _, _) when Typed.is_global_hyp s -> - let cnf = Cnf.make state.global td in - { state with global = cnf; } - | Typed.TAxiom (_, s, _, _) when Typed.is_local_hyp s -> - let cnf = Cnf.make state.local td in - { state with local = cnf; } - | _ -> - let cnf = Cnf.make state.ctx td in - { state with ctx = cnf; } - in - - let (module I : Input.S) = Input.find (Options.get_frontend ()) in - let parsed () = - try - Options.Time.start (); - Options.set_is_gui false; - I.parse_file ~content ~format:None - with - | Parsing.Parse_error -> - Printer.print_err "%a" Errors.report - (Syntax_error ((Lexing.dummy_pos,Lexing.dummy_pos),"")); - raise Exit - | Errors.Error e -> - begin match e with - | Errors.Run_error r -> begin - match r with - | Steps_limit _ -> - returned_status := - Worker_interface.LimitReached "Steps limit" - | _ -> returned_status := Worker_interface.Error "Run error" - end - | _ -> returned_status := Worker_interface.Error "Error" - end; - Printer.print_err "%a" Errors.report e; - raise Exit - in - let all_used_context = FE.init_all_used_context () in - let assertion_stack = Stack.create () in - let typing_loop state p = - try - let l, env = I.type_parsed state.env assertion_stack p in - List.fold_left (typed_loop all_used_context) { state with env; } l - with Errors.Error e -> - Printer.print_err "%a" Errors.report e; - raise Exit - in - - let state = { - env = I.empty_env; - ctx = []; - local = []; - global = []; - } in - - begin - try let _ : _ state = - Seq.fold_left typing_loop state (parsed ()) in () - with Exit -> () end; - - let compute_statistics () = - let used = - List.fold_left (fun acc ({Explanation.f;_} as r) -> - Util.MI.add (Expr.uid f) r acc - ) Util.MI.empty (!unsat_core) in - Hashtbl.fold (fun id (f,nb) acc -> - match Util.MI.find_opt id used with - | None -> begin - match Expr.form_view f with - | Lemma {name=name;loc=loc;_} -> - let b,e = loc in - let used = - if Options.get_unsat_core () then Worker_interface.Unused - else Worker_interface.Unknown in - (name,b.Lexing.pos_lnum,e.Lexing.pos_lnum,!nb,used) :: acc - | _ -> acc - end - | Some r -> - let b,e = r.loc in - (r.name,b.Lexing.pos_lnum,e.Lexing.pos_lnum,!nb,Worker_interface.Used) - :: acc - ) tbl [] - in -======= - let get_status_and_print status n = - returned_status := - begin match status with - | FE.Unsat _ -> Worker_interface.Unsat n - | FE.Inconsistent _ -> Worker_interface.Inconsistent n - | FE.Sat _ -> Worker_interface.Sat n - | FE.Unknown _ -> Worker_interface.Unknown n - | FE.Timeout _ -> Worker_interface.LimitReached "timeout" - | FE.Preprocess -> Worker_interface.Unknown n + let get_status_and_print status n = + returned_status := + begin match status with + | FE.Unsat _ -> Worker_interface.Unsat n + | FE.Inconsistent _ -> Worker_interface.Inconsistent n + | FE.Sat _ -> Worker_interface.Sat n + | FE.Unknown _ -> Worker_interface.Unknown n + | FE.Timeout _ -> Worker_interface.LimitReached "timeout" + | FE.Preprocess -> Worker_interface.Unknown n + end; + FE.print_status status n + in + + let solve all_context (cnf, goal_name) = + let used_context = FE.choose_used_context all_context ~goal_name in + let consistent_dep_stack = Stack.create () in + SAT.reset_refs (); + let _,_,dep = + List.fold_left + (FE.process_decl get_status_and_print used_context + Util.SS.empty consistent_dep_stack) + (SAT.empty_with_inst add_inst, true, Explanation.empty) cnf in + + if Options.get_unsat_core () then begin + unsat_core := Explanation.get_unsat_core dep; end; - FE.print_status status n - in - - let solve all_context used_names (cnf, goal_name) = - let used_context = FE.choose_used_context all_context ~goal_name in - let consistent_dep_stack = Stack.create () in - SAT.reset_refs (); - let _,_,dep = - List.fold_left - (FE.process_decl - get_status_and_print used_context used_names consistent_dep_stack) - (SAT.empty_with_inst add_inst, true, Explanation.empty) cnf in - - if Options.get_unsat_core () then begin - unsat_core := Explanation.get_unsat_core dep; - end; - in - - let typed_loop all_context used_names state td = - match td.Typed.c with - | Typed.TGoal (_, kind, name, _) -> - let l = state.local @ state.global @ state.ctx in - let cnf = List.rev @@ Cnf.make l td in - let () = solve all_context used_names (cnf, name) in - begin match kind with - | Typed.Check - | Typed.Cut -> { state with local = []; } - | Typed.Thm | Typed.Sat | Typed.AllSat _ -> - { state with global = []; local = []; } - end - | Typed.TAxiom (_, s, _, _) when Typed.is_global_hyp s -> - let cnf = Cnf.make state.global td in - { state with global = cnf; } - | Typed.TAxiom (_, s, _, _) when Typed.is_local_hyp s -> - let cnf = Cnf.make state.local td in - { state with local = cnf; } - | _ -> - let cnf = Cnf.make state.ctx td in - { state with ctx = cnf; } - in - - let (module I : Input.S) = Input.find (Options.get_frontend ()) in - let parsed () = - try - Options.Time.start (); - Options.set_is_gui false; - I.parse_file ~content ~format:None - with - | Parsing.Parse_error -> - Printer.print_err "%a" Errors.report - (Syntax_error ((Lexing.dummy_pos,Lexing.dummy_pos),"")); - raise Exit - | Errors.Error e -> - begin match e with - | Errors.Run_error r -> begin - match r with - | Steps_limit _ -> - returned_status := - Worker_interface.LimitReached "Steps limit" - | _ -> returned_status := Worker_interface.Error "Run error" - end - | _ -> returned_status := Worker_interface.Error "Error" + in + + let typed_loop all_context state td = + match td.Typed.c with + | Typed.TGoal (_, kind, name, _) -> + let l = state.local @ state.global @ state.ctx in + let cnf = List.rev @@ Cnf.make l td in + let () = solve all_context (cnf, name) in + begin match kind with + | Ty.Check + | Ty.Cut -> { state with local = []; } + | _ -> { state with global = []; local = []; } + end + | Typed.TAxiom (_, s, _, _) when Ty.is_global_hyp s -> + let cnf = Cnf.make state.global td in + { state with global = cnf; } + | Typed.TAxiom (_, s, _, _) when Ty.is_local_hyp s -> + let cnf = Cnf.make state.local td in + { state with local = cnf; } + | _ -> + let cnf = Cnf.make state.ctx td in + { state with ctx = cnf; } + in + + let (module I : Input.S) = Input.find (Options.get_frontend ()) in + let parsed () = + try + Options.Time.start (); + Options.set_is_gui false; + I.parse_file ~content ~format:None + with + | Parsing.Parse_error -> + Printer.print_err "%a" Errors.report + (Syntax_error ((Lexing.dummy_pos,Lexing.dummy_pos),"")); + raise Exit + | Errors.Error e -> + begin match e with + | Errors.Run_error r -> begin + match r with + | Steps_limit _ -> + returned_status := + Worker_interface.LimitReached "Steps limit" + | _ -> returned_status := Worker_interface.Error "Run error" + end + | _ -> returned_status := Worker_interface.Error "Error" + end; + Printer.print_err "%a" Errors.report e; + raise Exit + in + let all_used_context = FE.init_all_used_context () in + let assertion_stack = Stack.create () in + let typing_loop state p = + try + let l, env = I.type_parsed state.env assertion_stack p in + List.fold_left (typed_loop all_used_context) { state with env; } l + with Errors.Error e -> + Printer.print_err "%a" Errors.report e; + raise Exit + in + + let state = { + env = I.empty_env; + ctx = []; + local = []; + global = []; + } in + + begin + try let _ : _ state = + Seq.fold_left typing_loop state (parsed ()) in () + with Exit -> () end; + + let compute_statistics () = + let used = + List.fold_left (fun acc ({Explanation.f;_} as r) -> + Util.MI.add (Expr.uid f) r acc + ) Util.MI.empty (!unsat_core) in + Hashtbl.fold (fun id (f,nb) acc -> + match Util.MI.find_opt id used with + | None -> begin + match Expr.form_view f with + | Lemma {name=name;loc=loc;_} -> + let b,e = loc in + let used = + if Options.get_unsat_core () then Worker_interface.Unused + else Worker_interface.Unknown in + (name,b.Lexing.pos_lnum,e.Lexing.pos_lnum,!nb,used) :: acc + | _ -> acc + end + | Some r -> + let b,e = r.loc in + (r.name, b.Lexing.pos_lnum, e.Lexing.pos_lnum, !nb, + Worker_interface.Used) + :: acc + ) tbl [] + in + + let get_status_and_print status n = + returned_status := + begin match status with + | FE.Unsat _ -> Worker_interface.Unsat n + | FE.Inconsistent _ -> Worker_interface.Inconsistent n + | FE.Sat _ -> Worker_interface.Sat n + | FE.Unknown _ -> Worker_interface.Unknown n + | FE.Timeout _ -> Worker_interface.LimitReached "timeout" + | FE.Preprocess -> Worker_interface.Unknown n + end; + FE.print_status status n + in + + let solve all_context used_names (cnf, goal_name) = + let used_context = FE.choose_used_context all_context ~goal_name in + let consistent_dep_stack = Stack.create () in + SAT.reset_refs (); + let _,_,dep = + List.fold_left + (FE.process_decl + get_status_and_print used_context used_names consistent_dep_stack) + (SAT.empty_with_inst add_inst, true, Explanation.empty) cnf in + + if Options.get_unsat_core () then begin + unsat_core := Explanation.get_unsat_core dep; end; - Printer.print_err "%a" Errors.report e; - raise Exit - in - let all_used_context = FE.init_all_used_context () in - let assertion_stack = Stack.create () in - let typing_loop state p = - try - let l, env = I.type_parsed state.env assertion_stack p in - let used_names = I.get_env_logics state.env in - List.fold_left (typed_loop all_used_context used_names) - { state with env; } l - with Errors.Error e -> - Printer.print_err "%a" Errors.report e; - raise Exit - in - - let state = { - env = I.empty_env; - ctx = []; - local = []; - global = []; - } in - - begin - try let _ : _ state = - Seq.fold_left typing_loop state (parsed ()) in () - with Exit -> () end; - - let compute_statistics () = - let used = - List.fold_left (fun acc ({Explanation.f;_} as r) -> - Util.MI.add (Expr.uid f) r acc - ) Util.MI.empty (!unsat_core) in - Hashtbl.fold (fun id (f,nb) acc -> - match Util.MI.find_opt id used with - | None -> begin - match Expr.form_view f with - | Lemma {name=name;loc=loc;_} -> - let b,e = loc in - let used = - if Options.get_unsat_core () then Worker_interface.Unused - else Worker_interface.Unknown in - (name,b.Lexing.pos_lnum,e.Lexing.pos_lnum,!nb,used) :: acc - | _ -> acc - end - | Some r -> - let b,e = r.loc in - (r.name,b.Lexing.pos_lnum,e.Lexing.pos_lnum,!nb,Worker_interface.Used) - :: acc - ) tbl [] - in + in + + let typed_loop all_context used_names state td = + match td.Typed.c with + | Typed.TGoal (_, kind, name, _) -> + let l = state.local @ state.global @ state.ctx in + let cnf = List.rev @@ Cnf.make l td in + let () = solve all_context used_names (cnf, name) in + begin match kind with + | Ty.Check + | Ty.Cut -> { state with local = []; } + | Ty.Thm | Ty.Sat | Ty.AllSat _ -> + { state with global = []; local = []; } + end + | Typed.TAxiom (_, s, _, _) when Ty.is_global_hyp s -> + let cnf = Cnf.make state.global td in + { state with global = cnf; } + | Typed.TAxiom (_, s, _, _) when Ty.is_local_hyp s -> + let cnf = Cnf.make state.local td in + { state with local = cnf; } + | _ -> + let cnf = Cnf.make state.ctx td in + { state with ctx = cnf; } + in + + let (module I : Input.S) = Input.find (Options.get_frontend ()) in + let parsed () = + try + Options.Time.start (); + Options.set_is_gui false; + I.parse_file ~content ~format:None + with + | Parsing.Parse_error -> + Printer.print_err "%a" Errors.report + (Syntax_error ((Lexing.dummy_pos,Lexing.dummy_pos),"")); + raise Exit + | Errors.Error e -> + begin match e with + | Errors.Run_error r -> begin + match r with + | Steps_limit _ -> + returned_status := + Worker_interface.LimitReached "Steps limit" + | _ -> returned_status := Worker_interface.Error "Run error" + end + | _ -> returned_status := Worker_interface.Error "Error" + end; + Printer.print_err "%a" Errors.report e; + raise Exit + in + let all_used_context = FE.init_all_used_context () in + let assertion_stack = Stack.create () in + let typing_loop state p = + try + let l, env = I.type_parsed state.env assertion_stack p in + let used_names = I.get_env_logics state.env in + List.fold_left (typed_loop all_used_context used_names) + { state with env; } l + with Errors.Error e -> + Printer.print_err "%a" Errors.report e; + raise Exit + in + + let state = { + env = I.empty_env; + ctx = []; + local = []; + global = []; + } in + + begin + try let _ : _ state = + Seq.fold_left typing_loop state (parsed ()) in () + with Exit -> () end; + + let compute_statistics () = + let used = + List.fold_left (fun acc ({Explanation.f;_} as r) -> + Util.MI.add (Expr.uid f) r acc + ) Util.MI.empty (!unsat_core) in + Hashtbl.fold (fun id (f,nb) acc -> + match Util.MI.find_opt id used with + | None -> begin + match Expr.form_view f with + | Lemma {name=name;loc=loc;_} -> + let b,e = loc in + let used = + if Options.get_unsat_core () then Worker_interface.Unused + else Worker_interface.Unknown in + (name,b.Lexing.pos_lnum,e.Lexing.pos_lnum,!nb,used) :: acc + | _ -> acc + end + | Some r -> + let b,e = r.loc in + (r.name, b.Lexing.pos_lnum, e.Lexing.pos_lnum, !nb, + Worker_interface.Used) + :: acc + ) tbl [] + in (* returns a records with compatible worker_interface fields *) diff --git a/src/bin/text/main_text.ml b/src/bin/text/main_text.ml index 6bd5a6c50f..c24851d646 100644 --- a/src/bin/text/main_text.ml +++ b/src/bin/text/main_text.ml @@ -48,5 +48,7 @@ let () = Signals_profiling.init_signals (); Solving_loop.main () - (* let fun_decls = Seq.filter (function Parsed.Function_def _ -> true | _ -> false) parsed in *) +(* let fun_decls = + Seq.filter (function Parsed.Function_def _ -> true | _ -> false) parsed + in *) (* Models.sorts parsed; *) diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index 95a8d59f39..c944c07fdf 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -665,7 +665,7 @@ let two = Numbers.Q.from_int 2 let case_split env _ ~for_model ~to_optimize = if to_optimize != None || Options.get_disable_adts () - || not (Options.get_enable_adts_cs()) + || not (Options.get_enable_adts_cs()) then Sig_rel.Split [] else diff --git a/src/lib/reasoners/enum_rel.ml b/src/lib/reasoners/enum_rel.ml index 722dadaa42..d96e29e720 100644 --- a/src/lib/reasoners/enum_rel.ml +++ b/src/lib/reasoners/enum_rel.ml @@ -263,8 +263,8 @@ let case_split env uf ~for_model ~to_optimize = | Some (n,r,hs) -> let n = Numbers.Q.from_int n in if for_model || - Numbers.Q.compare - (Numbers.Q.mult n env.size_splits) (Options.get_max_split ()) <= 0 || + Numbers.Q.compare (Numbers.Q.mult n env.size_splits) + (Options.get_max_split ()) <= 0 || Numbers.Q.sign (Options.get_max_split ()) < 0 then let r' = Sh.is_mine (Cons (hs, X.type_info r)) in Debug.case_split r r'; diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 6097a4bcdc..420f864c72 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -1689,7 +1689,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct Debug.is_it_unsat gf; try (* let env = assume env env.pending_assumes in - let env = { env with pending_assumes = [] } in *) + let env = { env with pending_assumes = [] } in *) let guards_to_assume = ME.fold (fun _g gf_guard_with_ex acc -> gf_guard_with_ex :: acc @@ -1768,7 +1768,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct check_no_decision_in_env env; if true then (* TODO: fix regressions when we disable this option. *) -(* if Options.get_process_when_assuming() then *) + (* if Options.get_process_when_assuming() then *) try if Options.get_tableaux_cdcl () then cdcl_assume false env [add_guard env fg,dep]; diff --git a/src/lib/reasoners/intervalCalculus.ml b/src/lib/reasoners/intervalCalculus.ml index 465cc08d10..1a0fc35ed8 100644 --- a/src/lib/reasoners/intervalCalculus.ml +++ b/src/lib/reasoners/intervalCalculus.ml @@ -1753,14 +1753,14 @@ let fm_simplex_cube_integers_encoding env uf has_eqs = match rev_mx with | None -> simplex | Some _ -> - let max = bnd_to_simplex_bound (mx, ex_mx) in - fst @@ - (* assert upper bound -> inverted as a lower bound *) - if exists_in_simplex simplex xple then - Sim.Assert.var simplex xple ?max - else - Sim.Assert.poly - simplex (Sim.Core.P.from_list lple) xple ?max + let max = bnd_to_simplex_bound (mx, ex_mx) in + fst @@ + (* assert upper bound -> inverted as a lower bound *) + if exists_in_simplex simplex xple then + Sim.Assert.var simplex xple ?max + else + Sim.Assert.poly + simplex (Sim.Core.P.from_list lple) xple ?max in simplex ) simplex (int_constraints_from_map_intervals env uf) diff --git a/src/lib/reasoners/satml_frontend_hybrid.ml b/src/lib/reasoners/satml_frontend_hybrid.ml index a11240c2a4..7d1cf8ecb2 100644 --- a/src/lib/reasoners/satml_frontend_hybrid.ml +++ b/src/lib/reasoners/satml_frontend_hybrid.ml @@ -61,7 +61,7 @@ module Make (Th : Theory.S) = struct Some (l_ex, Atom.level p) else None | None -> - Util.failwith "No proxy formula for the formula %a" E.print f + Util.failwith "No proxy formula for the formula %a" E.print f let forget_decision env f lvl = let l_ok, _ = diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml index a3f68ea57a..933fff065e 100644 --- a/src/lib/reasoners/theory.ml +++ b/src/lib/reasoners/theory.ml @@ -694,8 +694,8 @@ module Main_Default : S = struct let res = List.fold_left (fun objectives (a, _, _) -> - match E.term_view a with - | {E.f = Sy.Op Sy.Optimize {order;is_max}; xs = [e]; _} -> + match E.term_view a with + | {E.f = Sy.Op Sy.Optimize {order;is_max}; xs = [e]; _} -> let r = try Uf.make uf e with Not_found -> diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli index 1cb0d5d3ba..043fcf8e3d 100644 --- a/src/lib/structures/ty.mli +++ b/src/lib/structures/ty.mli @@ -278,7 +278,7 @@ type goal_sort = (** The goal to be proved satisfiable *) | AllSat of string list (** Rather generate all models involving the given list of - propositional variables *) + propositional variables *) (** Goal sort. Used in typed declarations. *) val fresh_hypothesis_name : goal_sort -> string