Error locations in generated OCaml code - FStarLang/FStar GitHub Wiki

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).