You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Jonathan Protzenko edited this page Mar 25, 2016
·
2 revisions
The OCaml extraction backend of F★ generates so-called "location directives", so that backtraces and error messages locate errors in the original F★ files, rather than in the extracted OCaml files. Essentially, F★ generates once in a while a line of the form # X F where X is the original line number and F is the original file name. This modifies the OCaml parser's internal state.
Currently (02/11/2016), these lines are generated before every top-level binding and every let-binding. This means that some locations may be off by a few lines.
Use --no_location_info to disable this behavior (because, say, you're debugging F* itself).