Synth tactics are run during eager lax checking

[tchajed]

In the following example, after processing the first two lines, flycheck keeps re-running the failing tactic and displaying a tactic state due to lax checking. It would be best to ignore the synth_by_tactic during this eager syntax check and only run it when the last line is actually processed.

module Failing_tactic

open FStar.Tactics

let x: bool = synth_by_tactic (exact (quote 1))

[cpitclaudel]

@mtzguido added a new nosynth flag for that, but it does a bit too much ATM (it also disables typechecking for the tactic)

[cpitclaudel]

Should be fixed in cpitclaudel_staging.