Printing the goal fails if it has percent signs

[tchajed]

Looks like fstar-tactics--insert-goal doesn't escape the goal, directly using it as a format string. Evaluating the following results in the goal not being printed and an error "apply: Not enough arguments for format string".

module Percent_goal

open FStar.Tactics

let op_Percent = op_Addition

let foo () : Lemma True =
  assert_by_tactic (1%1 == 2) (dump "")

[tchajed]

Credit goes to @nickgian for finding this and identifying format strings as the problem.

[cpitclaudel]

Thanks. How silly.

[cpitclaudel]

I've pushed a slightly safer fix, too.