Inconsistent qualifiers when explicitly annotating a definition with a forall

[tchajed]

You can't annotate a let binding with a formula because of an automatic logic annotation:

module Logic_qual

val prop : Type0
let prop = forall (_:unit). True
(* Inconsistent qualifier annotations on prop; Expected {}, got {logic} *)

module Logic_qual2

logic val prop : Type0
let prop = forall (_:unit). True
(* The qualifier list "[logic logic]" is not permissible for this element: duplicate qualifiers *)

I can make the latter work by editing FStar.ToSyntax.ToSyntax.fst L2163 to not add a duplicate logic qualifier to let prop = .... FStar.ToSyntax.ToSyntax.fst L1689 should probably also be fixed. It's an unsatisfying conclusion since F* is adding a qualifier to a let binding and it's your job to fix the val to match; at the very least there should be an error asking you to add logic to the val.

[catalin-hritcu]

Problem seems similar to #638. One idea behind prop (#1048) was that we could also get rid of the logic qualifier.

[aseemr]

This is fixed in master. The logic qualifier is now deprecated and these errors no longer show up. Adding the example to the regressions.