Skip to content

Commit

Permalink
Merge pull request #3541 from mtzguido/nits
Browse files Browse the repository at this point in the history
Improving a few errors
  • Loading branch information
mtzguido authored Oct 8, 2024
2 parents 1b0f36d + cad84d9 commit 56a05cd
Show file tree
Hide file tree
Showing 4 changed files with 22 additions and 15 deletions.
15 changes: 12 additions & 3 deletions ocaml/fstar-lib/generated/FStar_Parser_Dep.ml

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

12 changes: 4 additions & 8 deletions ocaml/fstar-lib/generated/FStar_Syntax_DsEnv.ml

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

6 changes: 4 additions & 2 deletions src/parser/FStar.Parser.Dep.fst
Original file line number Diff line number Diff line change
Expand Up @@ -1521,8 +1521,10 @@ let collect (all_cmd_line_files: list file_name)
with_file_outchannel fn (fun outc -> print_graph outc fn dep_graph);
print_string "\n";
raise_error0 Errors.Fatal_CyclicDependence
(BU.format1 "Recursive dependency on module %s\n" filename)
raise_error0 Errors.Fatal_CyclicDependence [
text (BU.format1 "Recursive dependency on module %s." filename);
text "A full dependency graph was written to dep.graph.";
]
in
(* full_cycle_detection finds cycles across interface
boundaries that can otherwise be exploited to
Expand Down
4 changes: 2 additions & 2 deletions src/syntax/FStar.Syntax.DsEnv.fst
Original file line number Diff line number Diff line change
Expand Up @@ -1492,8 +1492,8 @@ let fail_or env lookup lid =
match resolve_module_name env modul true with
| None ->
let opened_modules = String.concat ", " opened_modules |> Errors.text in
msg @ [Errors.text (BU.format1 "Module %s does not belong to the list of modules in scope, namely:"
(string_of_lid modul)) ^^ subdoc opened_modules]
msg @ [Errors.text (BU.format1 "Could not resolve module name %s"
(string_of_lid modul))]
| Some modul' when (not (List.existsb (fun m -> m = (string_of_lid modul')) opened_modules)) ->
let opened_modules = String.concat ", " opened_modules |> Errors.text in
msg @ [Errors.text (BU.format2 "Module %s resolved into %s, which does not belong to the list of modules in scope, namely:"
Expand Down

0 comments on commit 56a05cd

Please sign in to comment.